Quelle  g_derive.mlg   Sprache: unbekannt

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

{

open Stdarg

}

DECLARE PLUGIN "rocq-runtime.plugins.derive"

{

let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))

let () =
   Mltop.add_init_function "rocq-runtime.plugins.derive" (fun () ->
     Procq.modify_keyword_state (fun kw -> CLexer.add_keyword_tok kw (Tok.PKEYWORD "SuchThat")))

let warn_deprecated_derive_suchthat =
   CWarnings.create ~name:"deprecated-derive-suchthat" ~category:Deprecation.Version.v9_0
  (fun () -> Pp.strbrk "Use of \"SuchThat\" and \"As\" in \"Derive\" is deprecated; replace them respectively by \"in\" and \"as\".")

}

VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof
| #[ atts = Vernacentries.DefAttributes.def_attributes; ]
  [ "Derive" open_binders(bl) "SuchThat" constr(suchthat) "As" identref(lemma) ] ->
  { warn_deprecated_derive_suchthat ();
    Derive.start_deriving ~atts bl suchthat lemma }
| #[ atts = Vernacentries.DefAttributes.def_attributes; ]
  [ "Derive" open_binders(bl) "in" constr(suchthat) "as" identref(lemma) ] ->
  { Derive.start_deriving ~atts bl suchthat lemma }
END