From e87288450d4d9e49ac91d179714a73bd0147c0d7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 19 May 2018 16:51:55 +0200 Subject: [api] Move `opacity_flag` to `Proof_global`. `Proof_global` is the main consumer of the flag, which doesn't seem to belong to the AST as plugins show. This will allow the vernac AST to be placed in `vernac` indeed. --- parsing/g_proofs.ml4 | 1 + plugins/derive/derive.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/funind/invfun.ml | 4 ++-- plugins/funind/recdef.ml | 8 ++++---- pretyping/vernacexpr.ml | 3 ++- printing/ppvernac.ml | 1 + proofs/proof_global.ml | 4 +++- proofs/proof_global.mli | 4 +++- stm/stm.ml | 6 +++--- vernac/lemmas.ml | 4 ++-- vernac/obligations.ml | 10 +++++----- vernac/vernacentries.ml | 2 +- 13 files changed, 29 insertions(+), 22 deletions(-) diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index e393c2bbfc..4f3d83a8a6 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -10,6 +10,7 @@ open Constrexpr open Vernacexpr +open Proof_global open Misctypes open Pcoq diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 8a55538bde..480819ebe1 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -61,7 +61,7 @@ let start_deriving f suchthat lemma = | Proved (opaque, None, obj) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> - opaque <> Vernacexpr.Transparent , f_def , lemma_def + opaque <> Proof_global.Transparent , f_def , lemma_def | _ -> assert false in (** The opacity of [f_def] is adjusted to be [false], as it diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 3801fec4b3..ccf109ce1b 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1013,7 +1013,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num lemma_type (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); - Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))); + Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))); evd diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 1809526356..b9d5ebf57c 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -818,7 +818,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i)))); - (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))); + (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)))); let finfo = find_Function_infos (fst f_as_constant) in (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *) let _,lem_cst_constr = Evd.fresh_global @@ -879,7 +879,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i)))) ; - (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))); + (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)))); let finfo = find_Function_infos (fst f_as_constant) in let _,lem_cst_constr = Evd.fresh_global (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2464c595f5..45c9eff2fc 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -72,7 +72,7 @@ let declare_fun f_id kind ?univs value = let ce = definition_entry ?univs value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; -let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None))) +let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Proof_global.Transparent,None))) let def_of_const t = match (Constr.kind t) with @@ -1306,9 +1306,9 @@ let build_new_goal_type () = let is_opaque_constant c = let cb = Global.lookup_constant c in match cb.Declarations.const_body with - | Declarations.OpaqueDef _ -> Vernacexpr.Opaque - | Declarations.Undef _ -> Vernacexpr.Opaque - | Declarations.Def _ -> Vernacexpr.Transparent + | Declarations.OpaqueDef _ -> Proof_global.Opaque + | Declarations.Undef _ -> Proof_global.Opaque + | Declarations.Def _ -> Proof_global.Transparent let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml index 304a5dadd5..71a2e8cb8f 100644 --- a/pretyping/vernacexpr.ml +++ b/pretyping/vernacexpr.ml @@ -135,7 +135,8 @@ type search_restriction = type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) -type opacity_flag = Opaque | Transparent +type opacity_flag = Proof_global.opacity_flag = Opaque | Transparent + [@ocaml.deprecated "Please use [Proof_global.opacity_flag]"] type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index f26ac0bf9a..7a34e80274 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -717,6 +717,7 @@ open Pputils return (keyword "Admitted") | VernacEndProof (Proved (opac,o)) -> return ( + let open Proof_global in match o with | None -> (match opac with | Transparent -> keyword "Defined" diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 97cfccb8de..d5cb5b09f9 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -78,9 +78,11 @@ type proof_object = { universes: UState.t; } +type opacity_flag = Opaque | Transparent + type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of Vernacexpr.opacity_flag * + | Proved of opacity_flag * Misctypes.lident option * proof_object diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index bf35fd6599..de4cec488a 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -48,10 +48,12 @@ type proof_object = { universes: UState.t; } +type opacity_flag = Opaque | Transparent + type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of Vernacexpr.opacity_flag * + | Proved of opacity_flag * Misctypes.lident option * proof_object type proof_terminator diff --git a/stm/stm.ml b/stm/stm.ml index 6b92e47378..b8fe8ddd78 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1511,7 +1511,7 @@ end = struct (* {{{ *) stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }) in + expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) @@ -1661,7 +1661,7 @@ end = struct (* {{{ *) let st = Vernacstate.freeze_interp_state `No in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; - expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }); + expr = VernacExpr ([], VernacEndProof (Proved (Proof_global.Opaque,None))) }); `OK proof end with e -> @@ -2121,7 +2121,7 @@ let collect_proof keep cur hd brkind id = | id :: _ -> Names.Id.to_string id in let loc = (snd cur).loc in let is_defined_expr = function - | VernacEndProof (Proved (Transparent,_)) -> true + | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true | _ -> false in let is_defined = function | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 3d627d2f6e..3c7ede3c99 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -334,8 +334,8 @@ let universe_proof_terminator compute_guard hook = Feedback.feedback Feedback.AddedAxiom | Proved (opaque,idopt,proof) -> let is_opaque, export_seff = match opaque with - | Vernacexpr.Transparent -> false, true - | Vernacexpr.Opaque -> true, false + | Transparent -> false, true + | Opaque -> true, false in let proof = get_proof proof compute_guard (hook (Some (proof.Proof_global.universes))) is_opaque in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 1e7721f8fe..3bf0ca0a87 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -849,12 +849,12 @@ let obligation_terminator name num guard hook auto pf = let obl = obls.(num) in let status = match obl.obl_status, opq with - | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp () - | (true, _), Vernacexpr.Opaque -> err_not_transp () - | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true - | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> + | (_, Evar_kinds.Expand), Opaque -> err_not_transp () + | (true, _), Opaque -> err_not_transp () + | (false, _), Opaque -> Evar_kinds.Define true + | (_, Evar_kinds.Define true), Transparent -> Evar_kinds.Define false - | (_, status), Vernacexpr.Transparent -> status + | (_, status), Transparent -> status in let obl = { obl with obl_status = false, status } in let ctx = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index eae8167c41..48deea97f8 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -518,7 +518,7 @@ let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) let status = Pfedit.by (Tactics.exact_proof c) in - save_proof (Vernacexpr.(Proved(Opaque,None))); + save_proof (Vernacexpr.(Proved(Proof_global.Opaque,None))); if not status then Feedback.feedback Feedback.AddedAxiom let vernac_assumption ~atts discharge kind l nl = -- cgit v1.2.3 From b4b515c2e61bc6ea662b48e84eb319ec8252b07d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 19 May 2018 16:54:01 +0200 Subject: [api] Move `Vernacexpr` to parsing. There were a few spurious dependencies on the `Vernac` AST in the pretyper, we remove them and move `Vernacexpr` and `Extend` to parsing, where they do belong more. --- META.coq | 4 +- interp/dumpglob.ml | 2 +- interp/dumpglob.mli | 4 +- interp/implicit_quantifiers.ml | 2 +- interp/implicit_quantifiers.mli | 2 +- parsing/extend.ml | 134 ++++++++++ parsing/parsing.mllib | 2 + parsing/vernacexpr.ml | 530 ++++++++++++++++++++++++++++++++++++++++ pretyping/extend.ml | 134 ---------- pretyping/pretyping.mllib | 2 - pretyping/vernacexpr.ml | 530 ---------------------------------------- vernac/vernacentries.ml | 4 +- 12 files changed, 675 insertions(+), 675 deletions(-) create mode 100644 parsing/extend.ml create mode 100644 parsing/vernacexpr.ml delete mode 100644 pretyping/extend.ml delete mode 100644 pretyping/vernacexpr.ml diff --git a/META.coq b/META.coq index 3414ccbd40..12d7666cb0 100644 --- a/META.coq +++ b/META.coq @@ -131,10 +131,10 @@ package "interp" ( package "grammar" ( - description = "Coq Base Grammar" + description = "Coq Camlp5 Grammar Extensions for Plugins" version = "8.8" - requires = "coq.interp" + requires = "camlp5.gramlib" directory = "grammar" archive(byte) = "grammar.cma" diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index bc6a1ef3aa..74618a2905 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -254,7 +254,7 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc -> let dump_definition {CAst.loc;v=id} sec s = dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id) -let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty = +let dump_constraint { CAst.loc; v = n } sec ty = match n with | Names.Name id -> dump_definition CAst.(make ?loc id) sec ty | Names.Anonymous -> () diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 8dfb4f8f7f..bf83d2df40 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -38,8 +38,8 @@ val dump_binding : ?loc:Loc.t -> Names.Id.Set.elt -> unit val dump_notation : (Constrexpr.notation * Notation.notation_location) Loc.located -> Notation_term.scope_name option -> bool -> unit -val dump_constraint : - Vernacexpr.typeclass_constraint -> bool -> string -> unit + +val dump_constraint : Misctypes.lname -> bool -> string -> unit val dump_string : string -> unit diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 58df9abc4a..289890544f 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -58,7 +58,7 @@ let in_generalizable : bool * Misctypes.lident list option -> obj = classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj) } -let declare_generalizable local gen = +let declare_generalizable ~local gen = Lib.add_anonymous_leaf (in_generalizable (local, gen)) let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 5f4129ae0c..39d0174f99 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -13,7 +13,7 @@ open Glob_term open Constrexpr open Libnames -val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit +val declare_generalizable : local:bool -> Misctypes.lident list option -> unit val ids_of_list : Id.t list -> Id.Set.t val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t diff --git a/parsing/extend.ml b/parsing/extend.ml new file mode 100644 index 0000000000..734b859f60 --- /dev/null +++ b/parsing/extend.ml @@ -0,0 +1,134 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* ('a list,'b list,'c list) ty_user_symbol +| TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol +| TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol +| TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol +| TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol +| TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol +| TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol + +(** {5 Type-safe grammar extension} *) + +type ('self, 'a) symbol = +| Atoken : Tok.t -> ('self, string) symbol +| Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol +| Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol +| Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol +| Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol +| Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol +| Aself : ('self, 'self) symbol +| Anext : ('self, 'self) symbol +| Aentry : 'a entry -> ('self, 'a) symbol +| Aentryl : 'a entry * int -> ('self, 'a) symbol +| Arules : 'a rules list -> ('self, 'a) symbol + +and ('self, _, 'r) rule = +| Stop : ('self, 'r, 'r) rule +| Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule + +and ('a, 'r) norec_rule = { norec_rule : 's. ('s, 'a, 'r) rule } + +and 'a rules = +| Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules + +type 'a production_rule = +| Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule + +type 'a single_extend_statment = + string option * + (** Level *) + gram_assoc option * + (** Associativity *) + 'a production_rule list + (** Symbol list with the interpretation function *) + +type 'a extend_statment = + gram_position option * + 'a single_extend_statment list diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index 1f29636b2e..103e1188a9 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,5 +1,7 @@ Tok CLexer +Extend +Vernacexpr Pcoq Egramml Egramcoq diff --git a/parsing/vernacexpr.ml b/parsing/vernacexpr.ml new file mode 100644 index 0000000000..6ebf66349c --- /dev/null +++ b/parsing/vernacexpr.ml @@ -0,0 +1,530 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Current, it contains the name of the coq version + which this notation is trying to be compatible with *) +type locality_flag = bool (* true = Local *) + +type option_value = Goptions.option_value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + | StringOptValue of string option + +type option_ref_value = + | StringRefValue of string + | QualidRefValue of reference + +(** Identifier and optional list of bound universes and constraints. *) + +type sort_expr = Sorts.family + +type definition_expr = + | ProveBody of local_binder_expr list * constr_expr + | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr + * constr_expr option + +type fixpoint_expr = + ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option + +type cofixpoint_expr = + ident_decl * local_binder_expr list * constr_expr * constr_expr option + +type local_decl_expr = + | AssumExpr of lname * constr_expr + | DefExpr of lname * constr_expr * constr_expr option + +type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *) +type decl_notation = lstring * constr_expr * scope_name option +type simple_binder = lident list * constr_expr +type class_binder = lident * constr_expr list +type 'a with_coercion = coercion_flag * 'a +type 'a with_instance = instance_flag * 'a +type 'a with_notation = 'a * decl_notation list +type 'a with_priority = 'a * int option +type constructor_expr = (lident * constr_expr) with_coercion +type constructor_list_or_record_decl_expr = + | Constructors of constructor_expr list + | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list +type inductive_expr = + ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind * + constructor_list_or_record_decl_expr + +type one_inductive_expr = + ident_decl * local_binder_expr list * constr_expr option * constructor_expr list + +type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr +and typeclass_context = typeclass_constraint list + +type proof_expr = + ident_decl * (local_binder_expr list * constr_expr) + +type syntax_modifier = + | SetItemLevel of string list * Extend.production_level + | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option + | SetLevel of int + | SetAssoc of Extend.gram_assoc + | SetEntryType of string * Extend.simple_constr_prod_entry_key + | SetOnlyParsing + | SetOnlyPrinting + | SetCompatVersion of Flags.compat_version + | SetFormat of string * lstring + +type proof_end = + | Admitted + (* name in `Save ident` when closing goal *) + | Proved of Proof_global.opacity_flag * lident option + +type scheme = + | InductionScheme of bool * reference or_by_notation * sort_expr + | CaseScheme of bool * reference or_by_notation * sort_expr + | EqualityScheme of reference or_by_notation + +type section_subset_expr = + | SsEmpty + | SsType + | SsSingl of lident + | SsCompl of section_subset_expr + | SsUnion of section_subset_expr * section_subset_expr + | SsSubstr of section_subset_expr * section_subset_expr + | SsFwdClose of section_subset_expr + +(** Extension identifiers for the VERNAC EXTEND mechanism. + + {b ("Extraction", 0} indicates {b Extraction {i qualid}} command. + + {b ("Extraction", 1} indicates {b Recursive Extraction {i qualid}} command. + + {b ("Extraction", 2)} indicates {b Extraction "{i filename}" {i qualid{_ 1}} ... {i qualid{_ n}}} command. + + {b ("ExtractionLibrary", 0)} indicates {b Extraction Library {i ident}} command. + + {b ("RecursiveExtractionLibrary", 0)} indicates {b Recursive Extraction Library {i ident}} command. + + {b ("SeparateExtraction", 0)} indicates {b Separate Extraction {i qualid{_ 1}} ... {i qualid{_ n}}} command. + + {b ("ExtractionLanguage", 0)} indicates {b Extraction Language Ocaml} or {b Extraction Language Haskell} or {b Extraction Language Scheme} or {b Extraction Language JSON} commands. + + {b ("ExtractionImplicit", 0)} indicates {b Extraction Implicit {i qualid} \[ {i ident{_1}} ... {i ident{_n} } \] } command. + + {b ("ExtractionConstant", 0)} indicates {b Extract Constant {i qualid} => {i string}} command. + + {b ("ExtractionInlinedConstant", 0)} indicates {b Extract Inlined Constant {i qualid} => {i string}} command. + + {b ("ExtractionInductive", 0)} indicates {b Extract Inductive {i qualid} => {i string} [ {i string} ... {string} ] {i optstring}} command. + + {b ("ExtractionBlacklist", 0)} indicates {b Extraction Blacklist {i ident{_1}} ... {i ident{_n}}} command. + *) +type extend_name = + (** Name of the vernac entry where the tactic is defined, typically found + after the VERNAC EXTEND statement in the source. *) + string * + (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch + is given an offset, starting from zero. *) + int + +(* This type allows registering the inlining of constants in native compiler. + It will be extended with primitive inductive types and operators *) +type register_kind = + | RegisterInline + +type bullet = Proof_bullet.t +[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"] + +(** {6 Types concerning the module layer} *) + +(** Rigid / flexible module signature *) + +type 'a module_signature = 'a Declaremods.module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) +[@@ocaml.deprecated "please use [Declaremods.module_signature]."] + +(** Which module inline annotations should we honor, + either None or the ones whose level is less or equal + to the given integer *) + +type inline = Declaremods.inline = + | NoInline + | DefaultInline + | InlineAt of int +[@@ocaml.deprecated "please use [Declaremods.inline]."] + +type module_ast_inl = module_ast * Declaremods.inline +type module_binder = bool option * lident list * module_ast_inl + +(** [Some b] if locally enabled/disabled according to [b], [None] if + we should use the global flag. *) +type vernac_cumulative = VernacCumulative | VernacNonCumulative + +(** {6 The type of vernacular expressions} *) + +type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit + +type vernac_argument_status = { + name : Name.t; + recarg_like : bool; + notation_scope : string CAst.t option; + implicit_status : vernac_implicit_status; +} + +type nonrec vernac_expr = + + | VernacLoad of verbose_flag * string + (* Syntax *) + | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) + | VernacOpenCloseScope of bool * scope_name + | VernacDelimiters of scope_name * string option + | VernacBindScope of scope_name * class_rawexpr list + | VernacInfix of (lstring * syntax_modifier list) * + constr_expr * scope_name option + | VernacNotation of + constr_expr * (lstring * syntax_modifier list) * + scope_name option + | VernacNotationAddFormat of string * string * string + + (* Gallina *) + | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr + | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list + | VernacEndProof of proof_end + | VernacExactProof of constr_expr + | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * + Declaremods.inline * (ident_decl list * constr_expr) with_coercion list + | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list + | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list + | VernacScheme of (lident option * scheme) list + | VernacCombinedScheme of lident * lident list + | VernacUniverse of lident list + | VernacConstraint of Glob_term.glob_constraint list + + (* Gallina extensions *) + | VernacBeginSection of lident + | VernacEndSegment of lident + | VernacRequire of + reference option * export_flag option * reference list + | VernacImport of export_flag * reference list + | VernacCanonical of reference or_by_notation + | VernacCoercion of reference or_by_notation * + class_rawexpr * class_rawexpr + | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr + | VernacNameSectionHypSet of lident * section_subset_expr + + (* Type classes *) + | VernacInstance of + bool * (* abstract instance *) + local_binder_expr list * (* super *) + typeclass_constraint * (* instance name, class name, params *) + (bool * constr_expr) option * (* props *) + Typeclasses.hint_info_expr + + | VernacContext of local_binder_expr list + + | VernacDeclareInstances of + (reference * Typeclasses.hint_info_expr) list (* instances names, priorities and patterns *) + + | VernacDeclareClass of reference (* inductive or definition name *) + + (* Modules and Module Types *) + | VernacDeclareModule of bool option * lident * + module_binder list * module_ast_inl + | VernacDefineModule of bool option * lident * module_binder list * + module_ast_inl Declaremods.module_signature * module_ast_inl list + | VernacDeclareModuleType of lident * + module_binder list * module_ast_inl list * module_ast_inl list + | VernacInclude of module_ast_inl list + + (* Solving *) + + | VernacSolveExistential of int * constr_expr + + (* Auxiliary file and library management *) + | VernacAddLoadPath of rec_flag * string * DirPath.t option + | VernacRemoveLoadPath of string + | VernacAddMLPath of rec_flag * string + | VernacDeclareMLModule of string list + | VernacChdir of string option + + (* State management *) + | VernacWriteState of string + | VernacRestoreState of string + + (* Resetting *) + | VernacResetName of lident + | VernacResetInitial + | VernacBack of int + | VernacBackTo of int + + (* Commands *) + | VernacCreateHintDb of string * bool + | VernacRemoveHints of string list * reference list + | VernacHints of string list * hints_expr + | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * + onlyparsing_flag + | VernacArguments of reference or_by_notation * + vernac_argument_status list (* Main arguments status list *) * + (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) * + int option (* Number of args to trigger reduction *) * + [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | + `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | + `DefaultImplicits ] list + | VernacReserve of simple_binder list + | VernacGeneralizable of (lident list) option + | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list) + | VernacSetStrategy of + (Conv_oracle.level * reference or_by_notation list) list + | VernacUnsetOption of export_flag * Goptions.option_name + | VernacSetOption of export_flag * Goptions.option_name * option_value + | VernacAddOption of Goptions.option_name * option_ref_value list + | VernacRemoveOption of Goptions.option_name * option_ref_value list + | VernacMemOption of Goptions.option_name * option_ref_value list + | VernacPrintOption of Goptions.option_name + | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr + | VernacGlobalCheck of constr_expr + | VernacDeclareReduction of string * Genredexpr.raw_red_expr + | VernacPrint of printable + | VernacSearch of searchable * Goal_select.t option * search_restriction + | VernacLocate of locatable + | VernacRegister of lident * register_kind + | VernacComments of comment list + + (* Proof management *) + | VernacAbort of lident option + | VernacAbortAll + | VernacRestart + | VernacUndo of int + | VernacUndoTo of int + | VernacFocus of int option + | VernacUnfocus + | VernacUnfocused + | VernacBullet of Proof_bullet.t + | VernacSubproof of Goal_select.t option + | VernacEndSubproof + | VernacShow of showable + | VernacCheckGuard + | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option + | VernacProofMode of string + + (* For extension *) + | VernacExtend of extend_name * Genarg.raw_generic_argument list + +type nonrec vernac_flag = + | VernacProgram + | VernacPolymorphic of bool + | VernacLocal of bool + +type vernac_control = + | VernacExpr of vernac_flag list * vernac_expr + (* boolean is true when the `-time` batch-mode command line flag was set. + the flag is used to print differently in `-time` vs `Time foo` *) + | VernacTime of bool * vernac_control CAst.t + | VernacRedirect of string * vernac_control CAst.t + | VernacTimeout of int * vernac_control + | VernacFail of vernac_control + +(* A vernac classifier provides information about the exectuion of a + command: + + - vernac_when: encodes if the vernac may alter the parser [thus + forcing immediate execution], or if indeed it is pure and parsing + can continue without its execution. + + - vernac_type: if it is starts, ends, continues a proof or + alters the global state or is a control command like BackTo or is + a query like Check. + + The classification works on the assumption that we have 3 states: + parsing, execution (global enviroment, etc...), and proof + state. For example, commands that only alter the proof state are + considered safe to delegate to a worker. + +*) +type vernac_type = + (* Start of a proof *) + | VtStartProof of vernac_start + (* Command altering the global state, bad for parallel + processing. *) + | VtSideff of vernac_sideff_type + (* End of a proof *) + | VtQed of vernac_qed_type + (* A proof step *) + | VtProofStep of proof_step + (* To be removed *) + | VtProofMode of string + (* Queries are commands assumed to be "pure", that is to say, they + don't modify the interpretation state. *) + | VtQuery + (* To be removed *) + | VtMeta + | VtUnknown +and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) +and vernac_start = string * opacity_guarantee * Id.t list +and vernac_sideff_type = Id.t list +and opacity_guarantee = + | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) + | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) +and proof_step = { (* TODO: inline with OCaml 4.03 *) + parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; + proof_block_detection : proof_block_name option +} +and solving_tac = bool (* a terminator *) +and anon_abstracting_tac = bool (* abstracting anonymously its result *) +and proof_block_name = string (* open type of delimiters *) +type vernac_when = + | VtNow + | VtLater +type vernac_classification = vernac_type * vernac_when + + +(** Deprecated stuff *) +type universe_decl_expr = Constrexpr.universe_decl_expr +[@@ocaml.deprecated "alias of Constrexpr.universe_decl_expr"] + +type ident_decl = Constrexpr.ident_decl +[@@ocaml.deprecated "alias of Constrexpr.ident_decl"] + +type name_decl = Constrexpr.name_decl +[@@ocaml.deprecated "alias of Constrexpr.name_decl"] diff --git a/pretyping/extend.ml b/pretyping/extend.ml deleted file mode 100644 index 734b859f60..0000000000 --- a/pretyping/extend.ml +++ /dev/null @@ -1,134 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* ('a list,'b list,'c list) ty_user_symbol -| TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol -| TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol -| TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol -| TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol -| TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol -| TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol - -(** {5 Type-safe grammar extension} *) - -type ('self, 'a) symbol = -| Atoken : Tok.t -> ('self, string) symbol -| Alist1 : ('self, 'a) symbol -> ('self, 'a list) symbol -| Alist1sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol -| Alist0 : ('self, 'a) symbol -> ('self, 'a list) symbol -| Alist0sep : ('self, 'a) symbol * ('self, _) symbol -> ('self, 'a list) symbol -| Aopt : ('self, 'a) symbol -> ('self, 'a option) symbol -| Aself : ('self, 'self) symbol -| Anext : ('self, 'self) symbol -| Aentry : 'a entry -> ('self, 'a) symbol -| Aentryl : 'a entry * int -> ('self, 'a) symbol -| Arules : 'a rules list -> ('self, 'a) symbol - -and ('self, _, 'r) rule = -| Stop : ('self, 'r, 'r) rule -| Next : ('self, 'a, 'r) rule * ('self, 'b) symbol -> ('self, 'b -> 'a, 'r) rule - -and ('a, 'r) norec_rule = { norec_rule : 's. ('s, 'a, 'r) rule } - -and 'a rules = -| Rules : ('act, Loc.t -> 'a) norec_rule * 'act -> 'a rules - -type 'a production_rule = -| Rule : ('a, 'act, Loc.t -> 'a) rule * 'act -> 'a production_rule - -type 'a single_extend_statment = - string option * - (** Level *) - gram_assoc option * - (** Associativity *) - 'a production_rule list - (** Symbol list with the interpretation function *) - -type 'a extend_statment = - gram_position option * - 'a single_extend_statment list diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index d98026bc60..c48decdb08 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -27,8 +27,6 @@ Pattern Patternops Constr_matching Tacred -Extend -Vernacexpr Typeclasses_errors Typeclasses Classops diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml deleted file mode 100644 index 71a2e8cb8f..0000000000 --- a/pretyping/vernacexpr.ml +++ /dev/null @@ -1,530 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Current, it contains the name of the coq version - which this notation is trying to be compatible with *) -type locality_flag = bool (* true = Local *) - -type option_value = Goptions.option_value = - | BoolValue of bool - | IntValue of int option - | StringValue of string - | StringOptValue of string option - -type option_ref_value = - | StringRefValue of string - | QualidRefValue of reference - -(** Identifier and optional list of bound universes and constraints. *) - -type sort_expr = Sorts.family - -type definition_expr = - | ProveBody of local_binder_expr list * constr_expr - | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr - * constr_expr option - -type fixpoint_expr = - ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option - -type cofixpoint_expr = - ident_decl * local_binder_expr list * constr_expr * constr_expr option - -type local_decl_expr = - | AssumExpr of lname * constr_expr - | DefExpr of lname * constr_expr * constr_expr option - -type inductive_kind = Inductive_kw | CoInductive | Variant | Record | Structure | Class of bool (* true = definitional, false = inductive *) -type decl_notation = lstring * constr_expr * scope_name option -type simple_binder = lident list * constr_expr -type class_binder = lident * constr_expr list -type 'a with_coercion = coercion_flag * 'a -type 'a with_instance = instance_flag * 'a -type 'a with_notation = 'a * decl_notation list -type 'a with_priority = 'a * int option -type constructor_expr = (lident * constr_expr) with_coercion -type constructor_list_or_record_decl_expr = - | Constructors of constructor_expr list - | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list -type inductive_expr = - ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind * - constructor_list_or_record_decl_expr - -type one_inductive_expr = - ident_decl * local_binder_expr list * constr_expr option * constructor_expr list - -type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr -and typeclass_context = typeclass_constraint list - -type proof_expr = - ident_decl * (local_binder_expr list * constr_expr) - -type syntax_modifier = - | SetItemLevel of string list * Extend.production_level - | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option - | SetLevel of int - | SetAssoc of Extend.gram_assoc - | SetEntryType of string * Extend.simple_constr_prod_entry_key - | SetOnlyParsing - | SetOnlyPrinting - | SetCompatVersion of Flags.compat_version - | SetFormat of string * lstring - -type proof_end = - | Admitted - (* name in `Save ident` when closing goal *) - | Proved of opacity_flag * lident option - -type scheme = - | InductionScheme of bool * reference or_by_notation * sort_expr - | CaseScheme of bool * reference or_by_notation * sort_expr - | EqualityScheme of reference or_by_notation - -type section_subset_expr = - | SsEmpty - | SsType - | SsSingl of lident - | SsCompl of section_subset_expr - | SsUnion of section_subset_expr * section_subset_expr - | SsSubstr of section_subset_expr * section_subset_expr - | SsFwdClose of section_subset_expr - -(** Extension identifiers for the VERNAC EXTEND mechanism. - - {b ("Extraction", 0} indicates {b Extraction {i qualid}} command. - - {b ("Extraction", 1} indicates {b Recursive Extraction {i qualid}} command. - - {b ("Extraction", 2)} indicates {b Extraction "{i filename}" {i qualid{_ 1}} ... {i qualid{_ n}}} command. - - {b ("ExtractionLibrary", 0)} indicates {b Extraction Library {i ident}} command. - - {b ("RecursiveExtractionLibrary", 0)} indicates {b Recursive Extraction Library {i ident}} command. - - {b ("SeparateExtraction", 0)} indicates {b Separate Extraction {i qualid{_ 1}} ... {i qualid{_ n}}} command. - - {b ("ExtractionLanguage", 0)} indicates {b Extraction Language Ocaml} or {b Extraction Language Haskell} or {b Extraction Language Scheme} or {b Extraction Language JSON} commands. - - {b ("ExtractionImplicit", 0)} indicates {b Extraction Implicit {i qualid} \[ {i ident{_1}} ... {i ident{_n} } \] } command. - - {b ("ExtractionConstant", 0)} indicates {b Extract Constant {i qualid} => {i string}} command. - - {b ("ExtractionInlinedConstant", 0)} indicates {b Extract Inlined Constant {i qualid} => {i string}} command. - - {b ("ExtractionInductive", 0)} indicates {b Extract Inductive {i qualid} => {i string} [ {i string} ... {string} ] {i optstring}} command. - - {b ("ExtractionBlacklist", 0)} indicates {b Extraction Blacklist {i ident{_1}} ... {i ident{_n}}} command. - *) -type extend_name = - (** Name of the vernac entry where the tactic is defined, typically found - after the VERNAC EXTEND statement in the source. *) - string * - (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch - is given an offset, starting from zero. *) - int - -(* This type allows registering the inlining of constants in native compiler. - It will be extended with primitive inductive types and operators *) -type register_kind = - | RegisterInline - -type bullet = Proof_bullet.t -[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"] - -(** {6 Types concerning the module layer} *) - -(** Rigid / flexible module signature *) - -type 'a module_signature = 'a Declaremods.module_signature = - | Enforce of 'a (** ... : T *) - | Check of 'a list (** ... <: T1 <: T2, possibly empty *) -[@@ocaml.deprecated "please use [Declaremods.module_signature]."] - -(** Which module inline annotations should we honor, - either None or the ones whose level is less or equal - to the given integer *) - -type inline = Declaremods.inline = - | NoInline - | DefaultInline - | InlineAt of int -[@@ocaml.deprecated "please use [Declaremods.inline]."] - -type module_ast_inl = module_ast * Declaremods.inline -type module_binder = bool option * lident list * module_ast_inl - -(** [Some b] if locally enabled/disabled according to [b], [None] if - we should use the global flag. *) -type vernac_cumulative = VernacCumulative | VernacNonCumulative - -(** {6 The type of vernacular expressions} *) - -type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit - -type vernac_argument_status = { - name : Name.t; - recarg_like : bool; - notation_scope : string CAst.t option; - implicit_status : vernac_implicit_status; -} - -type nonrec vernac_expr = - - | VernacLoad of verbose_flag * string - (* Syntax *) - | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) - | VernacOpenCloseScope of bool * scope_name - | VernacDelimiters of scope_name * string option - | VernacBindScope of scope_name * class_rawexpr list - | VernacInfix of (lstring * syntax_modifier list) * - constr_expr * scope_name option - | VernacNotation of - constr_expr * (lstring * syntax_modifier list) * - scope_name option - | VernacNotationAddFormat of string * string * string - - (* Gallina *) - | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr - | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list - | VernacEndProof of proof_end - | VernacExactProof of constr_expr - | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * - Declaremods.inline * (ident_decl list * constr_expr) with_coercion list - | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list - | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list - | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list - | VernacScheme of (lident option * scheme) list - | VernacCombinedScheme of lident * lident list - | VernacUniverse of lident list - | VernacConstraint of Glob_term.glob_constraint list - - (* Gallina extensions *) - | VernacBeginSection of lident - | VernacEndSegment of lident - | VernacRequire of - reference option * export_flag option * reference list - | VernacImport of export_flag * reference list - | VernacCanonical of reference or_by_notation - | VernacCoercion of reference or_by_notation * - class_rawexpr * class_rawexpr - | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr - | VernacNameSectionHypSet of lident * section_subset_expr - - (* Type classes *) - | VernacInstance of - bool * (* abstract instance *) - local_binder_expr list * (* super *) - typeclass_constraint * (* instance name, class name, params *) - (bool * constr_expr) option * (* props *) - Typeclasses.hint_info_expr - - | VernacContext of local_binder_expr list - - | VernacDeclareInstances of - (reference * Typeclasses.hint_info_expr) list (* instances names, priorities and patterns *) - - | VernacDeclareClass of reference (* inductive or definition name *) - - (* Modules and Module Types *) - | VernacDeclareModule of bool option * lident * - module_binder list * module_ast_inl - | VernacDefineModule of bool option * lident * module_binder list * - module_ast_inl Declaremods.module_signature * module_ast_inl list - | VernacDeclareModuleType of lident * - module_binder list * module_ast_inl list * module_ast_inl list - | VernacInclude of module_ast_inl list - - (* Solving *) - - | VernacSolveExistential of int * constr_expr - - (* Auxiliary file and library management *) - | VernacAddLoadPath of rec_flag * string * DirPath.t option - | VernacRemoveLoadPath of string - | VernacAddMLPath of rec_flag * string - | VernacDeclareMLModule of string list - | VernacChdir of string option - - (* State management *) - | VernacWriteState of string - | VernacRestoreState of string - - (* Resetting *) - | VernacResetName of lident - | VernacResetInitial - | VernacBack of int - | VernacBackTo of int - - (* Commands *) - | VernacCreateHintDb of string * bool - | VernacRemoveHints of string list * reference list - | VernacHints of string list * hints_expr - | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * - onlyparsing_flag - | VernacArguments of reference or_by_notation * - vernac_argument_status list (* Main arguments status list *) * - (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) * - int option (* Number of args to trigger reduction *) * - [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | - `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | - `DefaultImplicits ] list - | VernacReserve of simple_binder list - | VernacGeneralizable of (lident list) option - | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list) - | VernacSetStrategy of - (Conv_oracle.level * reference or_by_notation list) list - | VernacUnsetOption of export_flag * Goptions.option_name - | VernacSetOption of export_flag * Goptions.option_name * option_value - | VernacAddOption of Goptions.option_name * option_ref_value list - | VernacRemoveOption of Goptions.option_name * option_ref_value list - | VernacMemOption of Goptions.option_name * option_ref_value list - | VernacPrintOption of Goptions.option_name - | VernacCheckMayEval of Genredexpr.raw_red_expr option * Goal_select.t option * constr_expr - | VernacGlobalCheck of constr_expr - | VernacDeclareReduction of string * Genredexpr.raw_red_expr - | VernacPrint of printable - | VernacSearch of searchable * Goal_select.t option * search_restriction - | VernacLocate of locatable - | VernacRegister of lident * register_kind - | VernacComments of comment list - - (* Proof management *) - | VernacAbort of lident option - | VernacAbortAll - | VernacRestart - | VernacUndo of int - | VernacUndoTo of int - | VernacFocus of int option - | VernacUnfocus - | VernacUnfocused - | VernacBullet of Proof_bullet.t - | VernacSubproof of Goal_select.t option - | VernacEndSubproof - | VernacShow of showable - | VernacCheckGuard - | VernacProof of Genarg.raw_generic_argument option * section_subset_expr option - | VernacProofMode of string - - (* For extension *) - | VernacExtend of extend_name * Genarg.raw_generic_argument list - -type nonrec vernac_flag = - | VernacProgram - | VernacPolymorphic of bool - | VernacLocal of bool - -type vernac_control = - | VernacExpr of vernac_flag list * vernac_expr - (* boolean is true when the `-time` batch-mode command line flag was set. - the flag is used to print differently in `-time` vs `Time foo` *) - | VernacTime of bool * vernac_control CAst.t - | VernacRedirect of string * vernac_control CAst.t - | VernacTimeout of int * vernac_control - | VernacFail of vernac_control - -(* A vernac classifier provides information about the exectuion of a - command: - - - vernac_when: encodes if the vernac may alter the parser [thus - forcing immediate execution], or if indeed it is pure and parsing - can continue without its execution. - - - vernac_type: if it is starts, ends, continues a proof or - alters the global state or is a control command like BackTo or is - a query like Check. - - The classification works on the assumption that we have 3 states: - parsing, execution (global enviroment, etc...), and proof - state. For example, commands that only alter the proof state are - considered safe to delegate to a worker. - -*) -type vernac_type = - (* Start of a proof *) - | VtStartProof of vernac_start - (* Command altering the global state, bad for parallel - processing. *) - | VtSideff of vernac_sideff_type - (* End of a proof *) - | VtQed of vernac_qed_type - (* A proof step *) - | VtProofStep of proof_step - (* To be removed *) - | VtProofMode of string - (* Queries are commands assumed to be "pure", that is to say, they - don't modify the interpretation state. *) - | VtQuery - (* To be removed *) - | VtMeta - | VtUnknown -and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) -and vernac_start = string * opacity_guarantee * Id.t list -and vernac_sideff_type = Id.t list -and opacity_guarantee = - | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) - | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) -and proof_step = { (* TODO: inline with OCaml 4.03 *) - parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; - proof_block_detection : proof_block_name option -} -and solving_tac = bool (* a terminator *) -and anon_abstracting_tac = bool (* abstracting anonymously its result *) -and proof_block_name = string (* open type of delimiters *) -type vernac_when = - | VtNow - | VtLater -type vernac_classification = vernac_type * vernac_when - - -(** Deprecated stuff *) -type universe_decl_expr = Constrexpr.universe_decl_expr -[@@ocaml.deprecated "alias of Constrexpr.universe_decl_expr"] - -type ident_decl = Constrexpr.ident_decl -[@@ocaml.deprecated "alias of Constrexpr.ident_decl"] - -type name_decl = Constrexpr.name_decl -[@@ocaml.deprecated "alias of Constrexpr.name_decl"] diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 48deea97f8..e1ce4e194c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -855,7 +855,7 @@ let vernac_identity_coercion ~atts id qids qidt = let vernac_instance ~atts abst sup inst props pri = let global = not (make_section_locality atts.locality) in - Dumpglob.dump_constraint inst false "inst"; + Dumpglob.dump_constraint (fst (pi1 inst)) false "inst"; let program_mode = Flags.is_program_mode () in ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri) @@ -1268,7 +1268,7 @@ let vernac_reserve bl = let vernac_generalizable ~atts = let local = make_non_locality atts.locality in - Implicit_quantifiers.declare_generalizable local + Implicit_quantifiers.declare_generalizable ~local let _ = declare_bool_option -- cgit v1.2.3