diff options
133 files changed, 770 insertions, 741 deletions
diff --git a/CHANGES.md b/CHANGES.md index ca63d60a52..9a38b18a25 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -59,6 +59,10 @@ Tactics (e.g. `?[n]` or `?n` in terms - not in patterns) are now interpreted the same way as other variable names occurring in Ltac functions. +- Hint declaration and removal should now specify a database (e.g. `Hint Resolve + foo : database`). When the database name is omitted, the hint is added to the + core database (as previously), but a deprecation warning is emitted. + Vernacular commands - `Combined Scheme` can now work when inductive schemes are generated in sort @@ -69,6 +73,9 @@ Vernacular commands - Removed the deprecated `Implicit Tactic` family of commands. +- The `Automatic Introduction` option has been removed and is now the + default. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: @@ -95,6 +102,10 @@ Standard Library - Added `ByteVector` type that can convert to and from [string]. +- The prelude used to be automatically Exported and is now only + Imported. This should be relevant only when importing files which + don't use -noinit into files which do. + Universes - Added `Print Universes Subgraph` variant of `Print Universes`. diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index ba3b9bcbbf..8da4c6db13 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -374,9 +374,9 @@ let print_rules fmt rules = let print_classifier fmt = function | ClassifDefault -> fprintf fmt "" | ClassifName "QUERY" -> - fprintf fmt "~classifier:(fun _ -> Vernac_classifier.classify_as_query)" + fprintf fmt "~classifier:(fun _ -> Vernacextend.classify_as_query)" | ClassifName "SIDEFF" -> - fprintf fmt "~classifier:(fun _ -> Vernac_classifier.classify_as_sideeff)" + fprintf fmt "~classifier:(fun _ -> Vernacextend.classify_as_sideeff)" | ClassifName s -> fatal (Printf.sprintf "Unknown classifier %s" s) | ClassifCode c -> fprintf fmt "~classifier:(%s)" c.code diff --git a/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh b/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh new file mode 100644 index 0000000000..08112d3054 --- /dev/null +++ b/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "8902" ] || [ "$CI_BRANCH" = "ltac+use_atts_in_ast" ]; then + + aactactics_CI_REF=ltac+use_atts_in_ast + aactactics_CI_GITURL=https://github.com/ejgallego/aac-tactics + + coqhammer_CI_REF=ltac+use_atts_in_ast + coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer + + Equations_CI_REF=ltac+use_atts_in_ast + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + mtac2_CI_REF=ltac+use_atts_in_ast + mtac2_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh new file mode 100644 index 0000000000..61ffa4a197 --- /dev/null +++ b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9003" ] || [ "$CI_BRANCH" = "vernac+move_extend_ast" ]; then + + ltac2_CI_REF=vernac+move_extend_ast + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f94e9acb72..4287702b3a 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -514,18 +514,18 @@ let _ = let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in let cmd_fn c ~atts ~st = in_current_context econstr_display c; st in - let cmd_class _ = Vernacexpr.(VtQuery,VtNow) in + let cmd_class _ = VtQuery,VtNow in let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in - Vernacextend.vernac_extend ~command:"PrintConstr" [cmd] + vernac_extend ~command:"PrintConstr" [cmd] let _ = let open Vernacextend in let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in let cmd_fn c ~atts ~st = in_current_context print_pure_econstr c; st in - let cmd_class _ = Vernacexpr.(VtQuery,VtNow) in + let cmd_class _ = VtQuery,VtNow in let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in - Vernacextend.vernac_extend ~command:"PrintPureConstr" [cmd] + vernac_extend ~command:"PrintPureConstr" [cmd] (* Setting printer of unbound global reference *) open Names diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 741f9fe5b0..0b059f92ee 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -758,18 +758,6 @@ Controlling the effect of proof editing commands available hypotheses. -.. flag:: Automatic Introduction - - This option controls the way binders are handled - in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the - option is on, which is the default, binders are automatically put in - the local context of the goal to prove. - - When the option is off, binders are discharged on the statement to be - proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`) - has to be used to move the assumptions to the local context. - - .. flag:: Nested Proofs Allowed When turned on (it is off by default), this option enables support for nested diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index eacd7b4676..8f76085d88 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -167,7 +167,7 @@ Combined Scheme Combined Scheme tree_forest_mutind from tree_forest_ind,forest_tree_ind. - The type of tree_forest_mutrec will be: + The type of tree_forest_mutind will be: .. coqtop:: all diff --git a/engine/univNames.ml b/engine/univNames.ml index ad91d31f87..1019f8f0c2 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -36,10 +36,6 @@ type universe_binders = Univ.Level.t Names.Id.Map.t let empty_binders = Id.Map.empty -let universe_binders_of_global ref : Name.t array = - try AUContext.names (Environ.universes_of_global (Global.env ()) ref) - with Not_found -> [||] - let name_universe lvl = (** Best-effort naming from the string representation of the level. This is completely hackish and should be solved in upper layers instead. *) @@ -55,8 +51,8 @@ let compute_instance_binders inst ubinders = type univ_name_list = Names.lname list -let universe_binders_with_opt_names ref names = - let orig = universe_binders_of_global ref in +let universe_binders_with_opt_names orig names = + let orig = AUContext.names orig in let orig = Array.to_list orig in let udecl = match names with | None -> orig diff --git a/engine/univNames.mli b/engine/univNames.mli index dc669f45d6..6e68153ac2 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -29,5 +29,5 @@ type univ_name_list = Names.lname list of [ref] by [univs] (skipping Anonymous). May error if the lengths mismatch. Otherwise return the bound universe names registered for [ref]. *) -val universe_binders_with_opt_names : Names.GlobRef.t -> +val universe_binders_with_opt_names : AUContext.t -> univ_name_list option -> universe_binders diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml index 760410894a..1ce0136c1d 100644 --- a/gramlib/grammar.ml +++ b/gramlib/grammar.ml @@ -862,7 +862,6 @@ module type S = val parse_token_stream : 'a e -> te Stream.t -> 'a val print : Format.formatter -> 'a e -> unit external obj : 'a e -> te Gramext.g_entry = "%identity" - val parse_token : 'a e -> te Stream.t -> 'a end type ('self, 'a) ty_symbol type ('self, 'f, 'r) ty_rule @@ -930,18 +929,6 @@ module GMake (L : GLexerType) = Obj.magic (parse_parsable e p : Obj.t) let parse_token_stream (e : 'a e) ts : 'a = Obj.magic (e.estart 0 ts : Obj.t) - let _warned_using_parse_token = ref false - let parse_token (entry : 'a e) ts : 'a = - (* commented: too often warned in Coq... - if not warned_using_parse_token.val then do { - eprintf "<W> use of Entry.parse_token "; - eprintf "deprecated since 2017-06-16\n%!"; - eprintf "use Entry.parse_token_stream instead\n%! "; - warned_using_parse_token.val := True - } - else (); - *) - parse_token_stream entry ts let name e = e.ename let of_parser n (p : te Stream.t -> 'a) : 'a e = {egram = gram; ename = n; elocal = false; diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli index 244ab710dc..1c5fcb7bbf 100644 --- a/gramlib/grammar.mli +++ b/gramlib/grammar.mli @@ -36,7 +36,6 @@ module type S = val parse_token_stream : 'a e -> te Stream.t -> 'a val print : Format.formatter -> 'a e -> unit external obj : 'a e -> te Gramext.g_entry = "%identity" - val parse_token : 'a e -> te Stream.t -> 'a end type ('self, 'a) ty_symbol type ('self, 'f, 'r) ty_rule diff --git a/kernel/modops.ml b/kernel/modops.ml index bab2eae3df..0dde1c7e75 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -47,10 +47,9 @@ type signature_mismatch_error = | RecordFieldExpected of bool | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases - | IncompatibleInstances | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types - | IncompatibleConstraints of Univ.AUContext.t + | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t } type module_typing_error = | SignatureMismatch of diff --git a/kernel/modops.mli b/kernel/modops.mli index 8e7e618fcd..0acd09fb12 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -106,10 +106,9 @@ type signature_mismatch_error = | RecordFieldExpected of bool | RecordProjectionsExpected of Name.t list | NotEqualInductiveAliases - | IncompatibleInstances | IncompatibleUniverses of Univ.univ_inconsistency | IncompatiblePolymorphism of env * types * types - | IncompatibleConstraints of Univ.AUContext.t + | IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t } type module_typing_error = | SignatureMismatch of diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index d64342dbb0..347c30dd64 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -93,10 +93,8 @@ let check_conv_error error why cst poly f env a1 a2 = | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e) let check_polymorphic_instance error env auctx1 auctx2 = - if not (Univ.AUContext.size auctx1 == Univ.AUContext.size auctx2) then - error IncompatibleInstances - else if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then - error (IncompatibleConstraints auctx1) + if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then + error (IncompatibleConstraints { got = auctx1; expect = auctx2; } ) else Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env diff --git a/kernel/univ.ml b/kernel/univ.ml index 0edf750997..2b3b4f9486 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -570,9 +570,9 @@ struct include S let pr prl c = - fold (fun (u1,op,u2) pp_std -> - pp_std ++ prl u1 ++ pr_constraint_type op ++ - prl u2 ++ fnl () ) c (str "") + v 0 (prlist_with_sep spc (fun (u1,op,u2) -> + hov 0 (prl u1 ++ pr_constraint_type op ++ prl u2)) + (elements c)) end diff --git a/lib/flags.ml b/lib/flags.ml index 582506f3a8..3aef5a7b2c 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -99,10 +99,6 @@ let verbosely f x = without_option quiet f x let if_silent f x = if !quiet then f x let if_verbose f x = if not !quiet then f x -let auto_intros = ref true -let make_auto_intros flag = auto_intros := flag -let is_auto_intros () = !auto_intros - let polymorphic_inductive_cumulativity = ref false let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity diff --git a/lib/flags.mli b/lib/flags.mli index b667235678..e282d4ca8c 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -78,9 +78,6 @@ val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit (* Miscellaneus flags for vernac *) -val make_auto_intros : bool -> unit -val is_auto_intros : unit -> bool - val program_mode : bool ref val is_program_mode : unit -> bool diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index eb3e633892..d4aa598fd8 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -59,7 +59,7 @@ module type S = type e 'a = 'y; value create : string -> e 'a; value parse : e 'a -> parsable -> 'a; - value parse_token : e 'a -> Stream.t te -> 'a; + value parse_token_stream : e 'a -> Stream.t te -> 'a; value name : e 'a -> string; value of_parser : string -> (Stream.t te -> 'a) -> e 'a; value print : Format.formatter -> e 'a -> unit; diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v index f1095fc9f1..638a4cef21 100644 --- a/plugins/btauto/Algebra.v +++ b/plugins/btauto/Algebra.v @@ -10,7 +10,7 @@ end. Arguments decide P /H. -Hint Extern 5 => progress bool. +Hint Extern 5 => progress bool : core. Ltac define t x H := set (x := t) in *; assert (H : t = x) by reflexivity; clearbody x. @@ -147,7 +147,7 @@ Qed. (** * The core reflexive part. *) -Hint Constructors valid. +Hint Constructors valid : core. Fixpoint beq_poly pl pr := match pl with @@ -315,7 +315,7 @@ Section Validity. (* Decision procedure of validity *) -Hint Constructors valid linear. +Hint Constructors valid linear : core. Lemma valid_le_compat : forall k l p, valid k p -> (k <= l)%positive -> valid l p. Proof. @@ -425,10 +425,10 @@ match goal with | [ |- (?z < Pos.max ?x ?y)%positive ] => apply Pos.max_case_strong; intros; lia | _ => zify; omega -end. -Hint Resolve Pos.le_max_r Pos.le_max_l. +end : core. +Hint Resolve Pos.le_max_r Pos.le_max_l : core. -Hint Constructors valid linear. +Hint Constructors valid linear : core. (* Compatibility of validity w.r.t algebraic operations *) diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v index 4cde08872f..98f5ab067a 100644 --- a/plugins/btauto/Reflect.v +++ b/plugins/btauto/Reflect.v @@ -77,10 +77,10 @@ intros var f; induction f; simpl poly_of_formula; simpl formula_eval; auto. end. Qed. -Hint Extern 5 => change 0 with (min 0 0). -Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat. -Local Hint Constructors valid. -Hint Extern 5 => zify; omega. +Hint Extern 5 => change 0 with (min 0 0) : core. +Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat : core. +Local Hint Constructors valid : core. +Hint Extern 5 => zify; omega : core. (* Compatibility with validity *) diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index 18316bf2cd..df4b647642 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -18,7 +18,7 @@ DECLARE PLUGIN "derive_plugin" { -let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) +let classify_derive_command _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) } diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 1128a78093..a212d13453 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -66,7 +66,7 @@ let default_intuition_tac = let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in Tacenv.register_ml_tactic name [| tac |]; - Tacexpr.TacML (Loc.tag (entry, [])) + Tacexpr.TacML (CAst.make (entry, [])) let (set_default_solver, default_solver, print_default_solver) = Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver" diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d1e7d8a5a8..1cf952576d 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -320,10 +320,16 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* let dur1 = System.time_difference tim1 tim2 in *) (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) (* end; *) - get_proof_clean true, CEphemeron.create hook - end - + let open Proof_global in + let { id; entries; persistence } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in + match entries with + | [entry] -> + discard_current (); + (id,(entry,persistence)), CEphemeron.create hook + | _ -> + CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") + end let generate_functional_principle (evd: Evd.evar_map ref) interactive_proof diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 155df1c1e0..7e707b423a 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -186,8 +186,8 @@ VERNAC COMMAND EXTEND Function Vernac_classifier.classify_vernac (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with - | Vernacexpr.VtSideff ids, _ when hard -> - Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) + | Vernacextend.VtSideff ids, _ when hard -> + Vernacextend.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) | x -> x } -> { do_generate_principle false (List.map snd recsl) } END @@ -225,7 +225,7 @@ let warning_error names e = VERNAC COMMAND EXTEND NewFunctionalScheme | ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] - => { Vernacexpr.VtSideff(List.map pi1 fas), Vernacexpr.VtLater } + => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) } -> { begin @@ -261,7 +261,7 @@ END VERNAC COMMAND EXTEND NewFunctionalCase | ["Functional" "Case" fun_scheme_arg(fas) ] - => { Vernacexpr.VtSideff[pi1 fas], Vernacexpr.VtLater } + => { Vernacextend.(VtSideff[pi1 fas], VtLater) } -> { Functional_principles_types.build_case_scheme fas } END diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index cd2ea3ef88..b68b34ca35 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -147,17 +147,6 @@ let save with_clean id const (locality,_,kind) hook = CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); definition_message id - - -let cook_proof _ = - let (id,(entry,_,strength)) = Pfedit.cook_proof () in - (id,(entry,strength)) - -let get_proof_clean do_reduce = - let result = cook_proof do_reduce in - Proof_global.discard_current (); - result - let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 0c8f40c5cf..c9d153d89f 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -45,15 +45,6 @@ val jmeq_refl : unit -> EConstr.constr val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> Lemmas.declaration_hook CEphemeron.key -> unit -(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and - abort the proof -*) -val get_proof_clean : bool -> - Names.Id.t * - (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind) - - - (* [with_full_print f a] applies [f] to [a] in full printing environment. This function preserves the print settings diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index 6388906f5e..d9338f0421 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -333,7 +333,7 @@ open Tacexpr let initial_atomic () = let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in let iter (s, t) = - let body = TacAtom (Loc.tag t) in + let body = TacAtom (CAst.make t) in Tacenv.register_ltac false false (Names.Id.of_string s) body in let () = List.iter iter @@ -348,7 +348,7 @@ let initial_atomic () = List.iter iter [ "idtac",TacId []; "fail", TacFail(TacLocal,ArgArg 0,[]); - "fresh", TacArg(Loc.tag @@ TacFreshId []) + "fresh", TacArg(CAst.make @@ TacFreshId []) ] let () = Mltop.declare_cache_obj initial_atomic "ltac_plugin" @@ -379,8 +379,8 @@ let initial_tacticals () = let varn n = Reference (ArgVar (CAst.make (idn n))) in let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in List.iter iter [ - "first", TacFun ([Name (idn 0)], TacML (None, (initial_entry "first", [varn 0]))); - "solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0]))); + "first", TacFun ([Name (idn 0)], TacML (CAst.make (initial_entry "first", [varn 0]))); + "solve", TacFun ([Name (idn 0)], TacML (CAst.make (initial_entry "solve", [varn 0]))); ] let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin" diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 70e5ab38bc..603dd60cf2 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -31,6 +31,7 @@ open Tactypes open Tactics open Proofview.Notations open Attributes +open Vernacextend let wit_hyp = wit_var @@ -315,7 +316,7 @@ let add_rewrite_hint ~poly bases ort t lcsr = let add_hints base = add_rew_rules base eqs in List.iter add_hints bases -let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater +let classify_hint _ = VtSideff [], VtLater } @@ -398,7 +399,7 @@ END open Inv open Leminv -let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater +let seff id = VtSideff [id], VtLater } @@ -767,7 +768,7 @@ let case_eq_intros_rewrite x = let rec find_a_destructable_match sigma t = let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in let cl = [cl, (None, None), None], None in - let dest = TacAtom (Loc.tag @@ TacInductionDestruct(false, false, cl)) in + let dest = TacAtom (CAst.make @@ TacInductionDestruct(false, false, cl)) in match EConstr.kind sigma t with | Case (_,_,x,_) when closed0 sigma x -> if isVar sigma x then @@ -910,7 +911,7 @@ END mode. *) VERNAC COMMAND EXTEND GrabEvars | [ "Grab" "Existential" "Variables" ] - => { Vernac_classifier.classify_as_proofstep } + => { classify_as_proofstep } -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) } END @@ -942,7 +943,7 @@ END (* Command to add every unshelved variables to the focus *) VERNAC COMMAND EXTEND Unshelve | [ "Unshelve" ] - => { Vernac_classifier.classify_as_proofstep } + => { classify_as_proofstep } -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) } END @@ -1094,9 +1095,9 @@ END VERNAC COMMAND EXTEND OptimizeProof -| [ "Optimize" "Proof" ] => { Vernac_classifier.classify_as_proofstep } -> +| [ "Optimize" "Proof" ] => { classify_as_proofstep } -> { Proof_global.compact_the_proof () } -| [ "Optimize" "Heap" ] => { Vernac_classifier.classify_as_proofstep } -> +| [ "Optimize" "Heap" ] => { classify_as_proofstep } -> { Gc.compact () } END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index c58c8556c5..bd8a097154 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -33,7 +33,7 @@ open Pltac let fail_default_value = Locus.ArgArg 0 let arg_of_expr = function - TacArg (loc,a) -> a + TacArg { CAst.v } -> v | e -> Tacexp (e:raw_tactic_expr) let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () @@ -162,9 +162,9 @@ GRAMMAR EXTEND Gram | g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ]; l = LIST0 message_token -> { TacFail (g,n,l) } | st = simple_tactic -> { st } - | a = tactic_arg -> { TacArg(Loc.tag ~loc a) } + | a = tactic_arg -> { TacArg(CAst.make ~loc a) } | r = reference; la = LIST0 tactic_arg_compat -> - { TacArg(Loc.tag ~loc @@ TacCall (Loc.tag ~loc (r,la))) } ] + { TacArg(CAst.make ~loc @@ TacCall (CAst.make ~loc (r,la))) } ] | "0" [ "("; a = tactic_expr; ")" -> { a } | "["; ">"; tg = tactic_then_gen; "]" -> { @@ -173,7 +173,7 @@ GRAMMAR EXTEND Gram | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) | None -> TacDispatch tf end } - | a = tactic_atom -> { TacArg (Loc.tag ~loc a) } ] ] + | a = tactic_atom -> { TacArg (CAst.make ~loc a) } ] ] ; failkw: [ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ] @@ -223,7 +223,7 @@ GRAMMAR EXTEND Gram ; tactic_atom: [ [ n = integer -> { TacGeneric (genarg_of_int n) } - | r = reference -> { TacCall (Loc.tag ~loc (r,[])) } + | r = reference -> { TacCall (CAst.make ~loc (r,[])) } | "()" -> { TacGeneric (genarg_of_unit ()) } ] ] ; match_key: @@ -367,8 +367,7 @@ GRAMMAR EXTEND Gram open Stdarg open Tacarg -open Vernacexpr -open Vernac_classifier +open Vernacextend open Goptions open Libnames diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index aa78fb5d1e..e29f78af5b 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -84,7 +84,7 @@ open Obligations let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac -let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) +let classify_obbl _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) } diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 1c7220ddc0..2596bc22f2 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -26,6 +26,7 @@ open Pcoq.Prim open Pcoq.Constr open Pvernac.Vernac_ open Pltac +open Vernacextend let wit_hyp = wit_var @@ -280,18 +281,18 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF } | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) - => { Vernacexpr.VtUnknown, Vernacexpr.VtNow } + => { VtUnknown, VtNow } -> { add_morphism_infer atts m n; } | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) } + => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater } -> { add_morphism atts [] m s n; } | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) } + => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater } -> { add_morphism atts binders m s n; } diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 571595be70..0ce0fbd0cd 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -529,178 +529,178 @@ GRAMMAR EXTEND Gram [ [ (* Basic tactics *) IDENT "intros"; pl = ne_intropatterns -> - { TacAtom (Loc.tag ~loc @@ TacIntroPattern (false,pl)) } + { TacAtom (CAst.make ~loc @@ TacIntroPattern (false,pl)) } | IDENT "intros" -> - { TacAtom (Loc.tag ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) } + { TacAtom (CAst.make ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) } | IDENT "eintros"; pl = ne_intropatterns -> - { TacAtom (Loc.tag ~loc @@ TacIntroPattern (true,pl)) } + { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,pl)) } | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ","; - inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (true,false,cl,inhyp)) } + inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (true,false,cl,inhyp)) } | IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ","; - inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (true,true,cl,inhyp)) } + inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (true,true,cl,inhyp)) } | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ","; - inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (false,false,cl,inhyp)) } + inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (false,false,cl,inhyp)) } | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP","; - inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (false,true,cl,inhyp)) } + inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (false,true,cl,inhyp)) } | IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator -> - { TacAtom (Loc.tag ~loc @@ TacElim (false,cl,el)) } + { TacAtom (CAst.make ~loc @@ TacElim (false,cl,el)) } | IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator -> - { TacAtom (Loc.tag ~loc @@ TacElim (true,cl,el)) } - | IDENT "case"; icl = induction_clause_list -> { TacAtom (Loc.tag ~loc @@ mkTacCase false icl) } - | IDENT "ecase"; icl = induction_clause_list -> { TacAtom (Loc.tag ~loc @@ mkTacCase true icl) } + { TacAtom (CAst.make ~loc @@ TacElim (true,cl,el)) } + | IDENT "case"; icl = induction_clause_list -> { TacAtom (CAst.make ~loc @@ mkTacCase false icl) } + | IDENT "ecase"; icl = induction_clause_list -> { TacAtom (CAst.make ~loc @@ mkTacCase true icl) } | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl -> - { TacAtom (Loc.tag ~loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd)) } + { TacAtom (CAst.make ~loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd)) } | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl -> - { TacAtom (Loc.tag ~loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) } + { TacAtom (CAst.make ~loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) } | IDENT "pose"; bl = bindings_with_parameters -> - { let (id,b) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) } + { let (id,b) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) } | IDENT "pose"; b = constr; na = as_name -> - { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) } + { TacAtom (CAst.make ~loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) } | IDENT "epose"; bl = bindings_with_parameters -> - { let (id,b) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) } + { let (id,b) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) } | IDENT "epose"; b = constr; na = as_name -> - { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) } + { TacAtom (CAst.make ~loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) } | IDENT "set"; bl = bindings_with_parameters; p = clause_dft_concl -> - { let (id,c) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None)) } + { let (id,c) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None)) } | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl -> - { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,c,p,true,None)) } + { TacAtom (CAst.make ~loc @@ TacLetTac (false,na,c,p,true,None)) } | IDENT "eset"; bl = bindings_with_parameters; p = clause_dft_concl -> - { let (id,c) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (true,Names.Name id,c,p,true,None)) } + { let (id,c) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (true,Names.Name id,c,p,true,None)) } | IDENT "eset"; c = constr; na = as_name; p = clause_dft_concl -> - { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,c,p,true,None)) } + { TacAtom (CAst.make ~loc @@ TacLetTac (true,na,c,p,true,None)) } | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat; p = clause_dft_all -> - { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,c,p,false,e)) } + { TacAtom (CAst.make ~loc @@ TacLetTac (false,na,c,p,false,e)) } | IDENT "eremember"; c = constr; na = as_name; e = eqn_ipat; p = clause_dft_all -> - { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,c,p,false,e)) } + { TacAtom (CAst.make ~loc @@ TacLetTac (true,na,c,p,false,e)) } (* Alternative syntax for "pose proof c as id" *) | IDENT "assert"; test_lpar_id_coloneq; "("; lid = identref; ":="; c = lconstr; ")" -> { let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + TacAtom (CAst.make ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } | IDENT "eassert"; test_lpar_id_coloneq; "("; lid = identref; ":="; c = lconstr; ")" -> { let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + TacAtom (CAst.make ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } (* Alternative syntax for "assert c as id by tac" *) | IDENT "assert"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> { let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + TacAtom (CAst.make ?loc @@ TacAssert (false,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } | IDENT "eassert"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> { let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + TacAtom (CAst.make ?loc @@ TacAssert (true,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } (* Alternative syntax for "enough c as id by tac" *) | IDENT "enough"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> { let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + TacAtom (CAst.make ?loc @@ TacAssert (false,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } | IDENT "eenough"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> { let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + TacAtom (CAst.make ?loc @@ TacAssert (true,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic -> - { TacAtom (Loc.tag ~loc @@ TacAssert (false,true,Some tac,ipat,c)) } + { TacAtom (CAst.make ~loc @@ TacAssert (false,true,Some tac,ipat,c)) } | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic -> - { TacAtom (Loc.tag ~loc @@ TacAssert (true,true,Some tac,ipat,c)) } + { TacAtom (CAst.make ~loc @@ TacAssert (true,true,Some tac,ipat,c)) } | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> - { TacAtom (Loc.tag ~loc @@ TacAssert (false,true,None,ipat,c)) } + { TacAtom (CAst.make ~loc @@ TacAssert (false,true,None,ipat,c)) } | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> - { TacAtom (Loc.tag ~loc @@ TacAssert (true,true,None,ipat,c)) } + { TacAtom (CAst.make ~loc @@ TacAssert (true,true,None,ipat,c)) } | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic -> - { TacAtom (Loc.tag ~loc @@ TacAssert (false,false,Some tac,ipat,c)) } + { TacAtom (CAst.make ~loc @@ TacAssert (false,false,Some tac,ipat,c)) } | IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic -> - { TacAtom (Loc.tag ~loc @@ TacAssert (true,false,Some tac,ipat,c)) } + { TacAtom (CAst.make ~loc @@ TacAssert (true,false,Some tac,ipat,c)) } | IDENT "generalize"; c = constr -> - { TacAtom (Loc.tag ~loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) } + { TacAtom (CAst.make ~loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) } | IDENT "generalize"; c = constr; l = LIST1 constr -> { let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in - TacAtom (Loc.tag ~loc @@ TacGeneralize (List.map gen_everywhere (c::l))) } + TacAtom (CAst.make ~loc @@ TacGeneralize (List.map gen_everywhere (c::l))) } | IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs; na = as_name; l = LIST0 [","; c = pattern_occ; na = as_name -> { (c,na) } ] -> - { TacAtom (Loc.tag ~loc @@ TacGeneralize (((nl,c),na)::l)) } + { TacAtom (CAst.make ~loc @@ TacGeneralize (((nl,c),na)::l)) } (* Derived basic tactics *) | IDENT "induction"; ic = induction_clause_list -> - { TacAtom (Loc.tag ~loc @@ TacInductionDestruct (true,false,ic)) } + { TacAtom (CAst.make ~loc @@ TacInductionDestruct (true,false,ic)) } | IDENT "einduction"; ic = induction_clause_list -> - { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(true,true,ic)) } + { TacAtom (CAst.make ~loc @@ TacInductionDestruct(true,true,ic)) } | IDENT "destruct"; icl = induction_clause_list -> - { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(false,false,icl)) } + { TacAtom (CAst.make ~loc @@ TacInductionDestruct(false,false,icl)) } | IDENT "edestruct"; icl = induction_clause_list -> - { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(false,true,icl)) } + { TacAtom (CAst.make ~loc @@ TacInductionDestruct(false,true,icl)) } (* Equality and inversion *) | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; - cl = clause_dft_concl; t=by_tactic -> { TacAtom (Loc.tag ~loc @@ TacRewrite (false,l,cl,t)) } + cl = clause_dft_concl; t=by_tactic -> { TacAtom (CAst.make ~loc @@ TacRewrite (false,l,cl,t)) } | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; - cl = clause_dft_concl; t=by_tactic -> { TacAtom (Loc.tag ~loc @@ TacRewrite (true,l,cl,t)) } + cl = clause_dft_concl; t=by_tactic -> { TacAtom (CAst.make ~loc @@ TacRewrite (true,l,cl,t)) } | IDENT "dependent"; k = [ IDENT "simple"; IDENT "inversion" -> { SimpleInversion } | IDENT "inversion" -> { FullInversion } | IDENT "inversion_clear" -> { FullInversionClear } ]; hyp = quantified_hypothesis; ids = as_or_and_ipat; co = OPT ["with"; c = constr -> { c } ] -> - { TacAtom (Loc.tag ~loc @@ TacInversion (DepInversion (k,co,ids),hyp)) } + { TacAtom (CAst.make ~loc @@ TacInversion (DepInversion (k,co,ids),hyp)) } | IDENT "simple"; IDENT "inversion"; hyp = quantified_hypothesis; ids = as_or_and_ipat; cl = in_hyp_list -> - { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) } + { TacAtom (CAst.make ~loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) } | IDENT "inversion"; hyp = quantified_hypothesis; ids = as_or_and_ipat; cl = in_hyp_list -> - { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) } + { TacAtom (CAst.make ~loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) } | IDENT "inversion_clear"; hyp = quantified_hypothesis; ids = as_or_and_ipat; cl = in_hyp_list -> - { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) } + { TacAtom (CAst.make ~loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) } | IDENT "inversion"; hyp = quantified_hypothesis; "using"; c = constr; cl = in_hyp_list -> - { TacAtom (Loc.tag ~loc @@ TacInversion (InversionUsing (c,cl), hyp)) } + { TacAtom (CAst.make ~loc @@ TacInversion (InversionUsing (c,cl), hyp)) } (* Conversion *) | IDENT "red"; cl = clause_dft_concl -> - { TacAtom (Loc.tag ~loc @@ TacReduce (Red false, cl)) } + { TacAtom (CAst.make ~loc @@ TacReduce (Red false, cl)) } | IDENT "hnf"; cl = clause_dft_concl -> - { TacAtom (Loc.tag ~loc @@ TacReduce (Hnf, cl)) } + { TacAtom (CAst.make ~loc @@ TacReduce (Hnf, cl)) } | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> - { TacAtom (Loc.tag ~loc @@ TacReduce (Simpl (all_with d, po), cl)) } + { TacAtom (CAst.make ~loc @@ TacReduce (Simpl (all_with d, po), cl)) } | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl -> - { TacAtom (Loc.tag ~loc @@ TacReduce (Cbv s, cl)) } + { TacAtom (CAst.make ~loc @@ TacReduce (Cbv s, cl)) } | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl -> - { TacAtom (Loc.tag ~loc @@ TacReduce (Cbn s, cl)) } + { TacAtom (CAst.make ~loc @@ TacReduce (Cbn s, cl)) } | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl -> - { TacAtom (Loc.tag ~loc @@ TacReduce (Lazy s, cl)) } + { TacAtom (CAst.make ~loc @@ TacReduce (Lazy s, cl)) } | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl -> - { TacAtom (Loc.tag ~loc @@ TacReduce (Cbv (all_with delta), cl)) } + { TacAtom (CAst.make ~loc @@ TacReduce (Cbv (all_with delta), cl)) } | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> - { TacAtom (Loc.tag ~loc @@ TacReduce (CbvVm po, cl)) } + { TacAtom (CAst.make ~loc @@ TacReduce (CbvVm po, cl)) } | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> - { TacAtom (Loc.tag ~loc @@ TacReduce (CbvNative po, cl)) } + { TacAtom (CAst.make ~loc @@ TacReduce (CbvNative po, cl)) } | IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl -> - { TacAtom (Loc.tag ~loc @@ TacReduce (Unfold ul, cl)) } + { TacAtom (CAst.make ~loc @@ TacReduce (Unfold ul, cl)) } | IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl -> - { TacAtom (Loc.tag ~loc @@ TacReduce (Fold l, cl)) } + { TacAtom (CAst.make ~loc @@ TacReduce (Fold l, cl)) } | IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl -> - { TacAtom (Loc.tag ~loc @@ TacReduce (Pattern pl, cl)) } + { TacAtom (CAst.make ~loc @@ TacReduce (Pattern pl, cl)) } (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *) | IDENT "change"; c = conversion; cl = clause_dft_concl -> { let (oc, c) = c in let p,cl = merge_occurrences loc cl oc in - TacAtom (Loc.tag ~loc @@ TacChange (p,c,cl)) } + TacAtom (CAst.make ~loc @@ TacChange (p,c,cl)) } ] ] ; END diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index b219ee25ca..50cfb6d004 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -294,7 +294,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr _ = str "_" in KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)" - let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.tag arg)) + let pr_farg prtac arg = prtac (1, Any) (TacArg (CAst.make arg)) let is_genarg tag wit = let ArgT.Any tag = tag in @@ -350,9 +350,9 @@ let string_of_genarg_arg (ArgumentType arg) = pr_extend_gen (pr_farg prtac) let pr_raw_alias prtac lev key args = - pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args + pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (CAst.make a)))) lev key args let pr_glob_alias prtac lev key args = - pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args + pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (CAst.make a)))) lev key args (**********************************************************************) (* The tactic printer *) @@ -579,7 +579,7 @@ let pr_goal_selector ~toplevel s = pr_gen arg else str name ++ str ":" ++ surround (pr_gen arg) - | _ -> pr_arg (TacArg (Loc.tag t)) in + | _ -> pr_arg (TacArg (CAst.make t)) in hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++ str " :=" ++ brk (1,1) ++ pr t) @@ -1045,30 +1045,30 @@ let pr_goal_selector ~toplevel s = | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom | TacId l -> keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom - | TacAtom (loc,t) -> + | TacAtom { CAst.loc; v=t } -> pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom - | TacArg(_,Tacexp e) -> + | TacArg { CAst.v=Tacexp e } -> pr_tac inherited e, latom - | TacArg(_,ConstrMayEval (ConstrTerm c)) -> + | TacArg { CAst.v=ConstrMayEval (ConstrTerm c) } -> keyword "constr:" ++ pr.pr_constr c, latom - | TacArg(_,ConstrMayEval c) -> + | TacArg { CAst.v=ConstrMayEval c } -> pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval - | TacArg(_,TacFreshId l) -> + | TacArg { CAst.v=TacFreshId l } -> primitive "fresh" ++ pr_fresh_ids l, latom - | TacArg(_,TacGeneric arg) -> + | TacArg { CAst.v=TacGeneric arg } -> pr.pr_generic arg, latom - | TacArg(_,TacCall(_,(f,[]))) -> + | TacArg { CAst.v=TacCall {CAst.v=(f,[])} } -> pr.pr_reference f, latom - | TacArg(_,TacCall(loc,(f,l))) -> + | TacArg { CAst.v=TacCall {CAst.loc; v=(f,l)} } -> pr_with_comments ?loc (hov 1 ( pr.pr_reference f ++ spc () ++ prlist_with_sep spc pr_tacarg l)), lcall - | TacArg (_,a) -> + | TacArg { CAst.v=a } -> pr_tacarg a, latom - | TacML (loc,(s,l)) -> + | TacML { CAst.loc; v=(s,l) } -> pr_with_comments ?loc (pr.pr_extend 1 s l), lcall - | TacAlias (loc,(kn,l)) -> + | TacAlias { CAst.loc; v=(kn,l) } -> pr_with_comments ?loc (pr.pr_alias (level_of inherited) kn l), latom ) in @@ -1087,7 +1087,7 @@ let pr_goal_selector ~toplevel s = | TacNumgoals -> keyword "numgoals" | (TacCall _|Tacexp _ | TacGeneric _) as a -> - hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.tag a)))) + hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (CAst.make a)))) in pr_tac diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index db7dcfa6ef..3eb049dbab 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -251,7 +251,7 @@ let string_of_call ck = | Tacexpr.LtacVarCall (id, t) -> Names.Id.print id | Tacexpr.LtacAtomCall te -> (Pptactic.pr_glob_tactic (Global.env ()) - (Tacexpr.TacAtom (Loc.tag te))) + (Tacexpr.TacAtom (CAst.make te))) | Tacexpr.LtacConstrInterp (c, _) -> pr_glob_constr_env (Global.env ()) c | Tacexpr.LtacMLCall te -> diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 4142fb2412..fee469032c 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1958,7 +1958,7 @@ let add_setoid atts binders a aeq t n = let make_tactic name = let open Tacexpr in let tacqid = Libnames.qualid_of_string name in - TacArg (Loc.tag @@ (TacCall (Loc.tag (tacqid, [])))) + TacArg (CAst.make @@ (TacCall (CAst.make (tacqid, [])))) let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 1b212334ce..188d5de7de 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -177,7 +177,7 @@ let add_tactic_entry (kn, ml, tg) state = TacGeneric arg in let l = List.map map l in - (TacAlias (Loc.tag ~loc (kn,l)):raw_tactic_expr) + (TacAlias (CAst.make ~loc (kn,l)):raw_tactic_expr) in let () = if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then @@ -349,7 +349,7 @@ let extend_atomic_tactic name entries = | TacNonTerm (_, (symb, _)) -> let EntryName (typ, e) = prod_item_of_symbol 0 symb in let Genarg.Rawwit wit = typ in - let inj x = TacArg (Loc.tag @@ TacGeneric (Genarg.in_gen typ x)) in + let inj x = TacArg (CAst.make @@ TacGeneric (Genarg.in_gen typ x)) in let default = epsilon_value inj e in match default with | None -> raise NonEmptyArgument @@ -363,7 +363,7 @@ let extend_atomic_tactic name entries = | Some (id, args) -> let args = List.map (fun a -> Tacexp a) args in let entry = { mltac_name = name; mltac_index = i } in - let body = TacML (Loc.tag (entry, args)) in + let body = TacML (CAst.make (entry, args)) in Tacenv.register_ltac false false (Names.Id.of_string id) body in List.iteri add_atomic entries @@ -379,7 +379,7 @@ let add_ml_tactic_notation name ~level ?deprecation prods = let ids = List.map_filter get_id prods in let entry = { mltac_name = name; mltac_index = len - i - 1 } in let map id = Reference (Locus.ArgVar (CAst.make id)) in - let tac = TacML (Loc.tag (entry, List.map map ids)) in + let tac = TacML (CAst.make (entry, List.map map ids)) in add_glob_tactic_notation false ~level ?deprecation prods true ids tac in List.iteri iter (List.rev prods); @@ -664,7 +664,7 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign = (** Arguments are not passed directly to the ML tactic in the TacML node, the ML tactic retrieves its arguments in the [ist] environment instead. This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) - let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in + let body = Tacexpr.TacFun (vars, Tacexpr.TacML (CAst.make (ml, [])))in let id = Names.Id.of_string name in let obj () = Tacenv.register_ltac true false id body ?deprecation in let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 8731cbf60d..9435d0b911 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -167,7 +167,7 @@ type 'a gen_tactic_arg = | TacGeneric of 'lev generic_argument | ConstrMayEval of ('trm,'cst,'pat) may_eval | Reference of 'ref - | TacCall of ('ref * 'a gen_tactic_arg list) Loc.located + | TacCall of ('ref * 'a gen_tactic_arg list) CAst.t | TacFreshId of string or_var list | Tacexp of 'tacexpr | TacPretype of 'trm @@ -189,7 +189,7 @@ constraint 'a = < 'r : ltac refs, 'n : idents, 'l : levels *) and 'a gen_tactic_expr = - | TacAtom of ('a gen_atomic_tactic_expr) Loc.located + | TacAtom of ('a gen_atomic_tactic_expr) CAst.t | TacThen of 'a gen_tactic_expr * 'a gen_tactic_expr @@ -245,12 +245,12 @@ and 'a gen_tactic_expr = | TacMatchGoal of lazy_flag * direction_flag * ('p,'a gen_tactic_expr) match_rule list | TacFun of 'a gen_tactic_fun_ast - | TacArg of 'a gen_tactic_arg located + | TacArg of 'a gen_tactic_arg CAst.t | TacSelect of Goal_select.t * 'a gen_tactic_expr (* For ML extensions *) - | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located + | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) CAst.t (* For syntax extensions *) - | TacAlias of (KerName.t * 'a gen_tactic_arg list) Loc.located + | TacAlias of (KerName.t * 'a gen_tactic_arg list) CAst.t constraint 'a = < term:'t; diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 9958d6dcda..1527724420 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -167,7 +167,7 @@ type 'a gen_tactic_arg = | TacGeneric of 'lev generic_argument | ConstrMayEval of ('trm,'cst,'pat) may_eval | Reference of 'ref - | TacCall of ('ref * 'a gen_tactic_arg list) Loc.located + | TacCall of ('ref * 'a gen_tactic_arg list) CAst.t | TacFreshId of string or_var list | Tacexp of 'tacexpr | TacPretype of 'trm @@ -189,7 +189,7 @@ constraint 'a = < 'r : ltac refs, 'n : idents, 'l : levels *) and 'a gen_tactic_expr = - | TacAtom of ('a gen_atomic_tactic_expr) Loc.located + | TacAtom of ('a gen_atomic_tactic_expr) CAst.t | TacThen of 'a gen_tactic_expr * 'a gen_tactic_expr @@ -245,12 +245,12 @@ and 'a gen_tactic_expr = | TacMatchGoal of lazy_flag * direction_flag * ('p,'a gen_tactic_expr) match_rule list | TacFun of 'a gen_tactic_fun_ast - | TacArg of 'a gen_tactic_arg located + | TacArg of 'a gen_tactic_arg CAst.t | TacSelect of Goal_select.t * 'a gen_tactic_expr (* For ML extensions *) - | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located + | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) CAst.t (* For syntax extensions *) - | TacAlias of (KerName.t * 'a gen_tactic_arg list) Loc.located + | TacAlias of (KerName.t * 'a gen_tactic_arg list) CAst.t constraint 'a = < term:'t; diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index ebec3c887c..85c6348b52 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -137,7 +137,7 @@ let intern_isolated_global_tactic_reference qid = let kn = Tacenv.locate_tactic qid in Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@ Tacenv.tac_deprecation kn; - TacCall (Loc.tag ?loc (ArgArg (loc,kn),[])) + TacCall (CAst.make ?loc (ArgArg (loc,kn),[])) let intern_isolated_tactic_reference strict ist qid = (* An ltac reference *) @@ -587,10 +587,10 @@ let rec intern_atomic lf ist x = and intern_tactic onlytac ist tac = snd (intern_tactic_seq onlytac ist tac) and intern_tactic_seq onlytac ist = function - | TacAtom (loc,t) -> + | TacAtom { loc; v=t } -> let lf = ref ist.ltacvars in let t = intern_atomic lf ist t in - !lf, TacAtom (Loc.tag ?loc:(adjust_loc loc) t) + !lf, TacAtom (CAst.make ?loc:(adjust_loc loc) t) | TacFun tacfun -> ist.ltacvars, TacFun (intern_tactic_fun ist tacfun) | TacLetIn (isrec,l,u) -> let ltacvars = Id.Set.union (extract_let_names l) ist.ltacvars in @@ -659,27 +659,27 @@ and intern_tactic_seq onlytac ist = function | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_pure_tactic ist) l) | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_pure_tactic ist) l) | TacComplete tac -> ist.ltacvars, TacComplete (intern_pure_tactic ist tac) - | TacArg (loc,a) -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a + | TacArg { loc; v=a } -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a | TacSelect (sel, tac) -> ist.ltacvars, TacSelect (sel, intern_pure_tactic ist tac) (* For extensions *) - | TacAlias (loc,(s,l)) -> + | TacAlias { loc; v=(s,l) } -> let alias = Tacenv.interp_alias s in Option.iter (fun o -> warn_deprecated_alias ?loc (s,o)) @@ alias.Tacenv.alias_deprecation; let l = List.map (intern_tacarg !strict_check false ist) l in - ist.ltacvars, TacAlias (Loc.tag ?loc (s,l)) - | TacML (loc,(opn,l)) -> + ist.ltacvars, TacAlias (CAst.make ?loc (s,l)) + | TacML { loc; v=(opn,l) } -> let _ignore = Tacenv.interp_ml_tactic opn in - ist.ltacvars, TacML (loc, (opn,List.map (intern_tacarg !strict_check false ist) l)) + ist.ltacvars, TacML CAst.(make ?loc (opn,List.map (intern_tacarg !strict_check false ist) l)) and intern_tactic_as_arg loc onlytac ist a = match intern_tacarg !strict_check onlytac ist a with | TacCall _ | Reference _ - | TacGeneric _ as a -> TacArg (loc,a) + | TacGeneric _ as a -> TacArg CAst.(make ?loc a) | Tacexp a -> a | ConstrMayEval _ | TacFreshId _ | TacPretype _ | TacNumgoals as a -> - if onlytac then error_tactic_expected ?loc else TacArg (loc,a) + if onlytac then error_tactic_expected ?loc else TacArg CAst.(make ?loc a) and intern_tactic_or_tacarg ist = intern_tactic false ist @@ -692,9 +692,9 @@ and intern_tactic_fun ist (var,body) = and intern_tacarg strict onlytac ist = function | Reference r -> intern_non_tactic_reference strict ist r | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c) - | TacCall (loc,(f,[])) -> intern_isolated_tactic_reference strict ist f - | TacCall (loc,(f,l)) -> - TacCall (Loc.tag ?loc ( + | TacCall { loc; v=(f,[]) } -> intern_isolated_tactic_reference strict ist f + | TacCall { loc; v=(f,l) } -> + TacCall (CAst.make ?loc ( intern_applied_tactic_reference ist f, List.map (intern_tacarg !strict_check false ist) l)) | TacFreshId x -> TacFreshId (List.map (intern_string_or_var ist) x) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 5bfb0f79fb..cb3a0aaed9 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1018,7 +1018,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti | TacLetIn (false,l,u) -> interp_letin ist l u | TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist lz lr lmr | TacMatch (lz,c,lmr) -> interp_match ist lz c lmr - | TacArg (loc,a) -> interp_tacarg ist a + | TacArg {loc;v} -> interp_tacarg ist v | t -> (** Delayed evaluation *) Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], t))) @@ -1036,7 +1036,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti and eval_tactic ist tac : unit Proofview.tactic = match tac with - | TacAtom (loc,t) -> + | TacAtom {loc;v=t} -> let call = LtacAtomCall t in push_trace(loc,call) ist >>= fun trace -> Profile_ltac.do_profile "eval_tactic:2" trace @@ -1116,7 +1116,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with eval_tactic ist tac | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) - | TacAlias (loc,(s,l)) -> + | TacAlias {loc; v=(s,l)} -> let alias = Tacenv.interp_alias s in let (>>=) = Ftactic.bind in let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in @@ -1147,7 +1147,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with in Ftactic.run tac (fun () -> Proofview.tclUNIT ()) - | TacML (loc,(opn,l)) -> + | TacML {loc; v=(opn,l)} -> push_trace (Loc.tag ?loc @@ LtacMLCall tac) ist >>= fun trace -> let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in let tac = Tacenv.interp_ml_tactic opn in @@ -1201,9 +1201,9 @@ and interp_tacarg ist arg : Val.t Ftactic.t = Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Ftactic.return (Value.of_constr c_interp)) end - | TacCall (loc,(r,[])) -> + | TacCall { v=(r,[]) } -> interp_ltac_reference true ist r - | TacCall (loc,(f,l)) -> + | TacCall { loc; v=(f,l) } -> let (>>=) = Ftactic.bind in interp_ltac_reference true ist f >>= fun fv -> Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs -> @@ -1337,7 +1337,7 @@ and interp_letrec ist llc u = Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *) let lref = ref ist.lfun in let fold accu ({v=na}, b) = - let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in + let v = of_tacvalue (VRec (lref, TacArg (CAst.make b))) in Name.fold_right (fun id -> Id.Map.add id v) na accu in let lfun = List.fold_left fold ist.lfun llc in @@ -1875,7 +1875,7 @@ module Value = struct let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in let lfun = Id.Map.add (Id.of_string "F") f lfun in let ist = { (default_ist ()) with lfun = lfun; } in - let tac = TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string "F"),args))) in + let tac = TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) in eval_tactic_ist ist tac end diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 9173e23b89..caaa547a07 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -173,7 +173,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with TacInversion (InversionUsing (subst_glob_constr subst c,cl),hyp) and subst_tactic subst (t:glob_tactic_expr) = match t with - | TacAtom (_loc,t) -> TacAtom (Loc.tag @@ subst_atomic subst t) + | TacAtom { CAst.v=t } -> TacAtom (CAst.make @@ subst_atomic subst t) | TacFun tacfun -> TacFun (subst_tactic_fun subst tacfun) | TacLetIn (r,l,u) -> let l = List.map (fun (n,b) -> (n,subst_tacarg subst b)) l in @@ -220,22 +220,22 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacFirst l -> TacFirst (List.map (subst_tactic subst) l) | TacSolve l -> TacSolve (List.map (subst_tactic subst) l) | TacComplete tac -> TacComplete (subst_tactic subst tac) - | TacArg (_,a) -> TacArg (Loc.tag @@ subst_tacarg subst a) + | TacArg { CAst.v=a } -> TacArg (CAst.make @@ subst_tacarg subst a) | TacSelect (s, tac) -> TacSelect (s, subst_tactic subst tac) (* For extensions *) - | TacAlias (_,(s,l)) -> + | TacAlias { CAst.v=(s,l) } -> let s = subst_kn subst s in - TacAlias (Loc.tag (s,List.map (subst_tacarg subst) l)) - | TacML (loc,(opn,l)) -> TacML (loc, (opn,List.map (subst_tacarg subst) l)) + TacAlias (CAst.make (s,List.map (subst_tacarg subst) l)) + | TacML { CAst.loc; v=(opn,l)} -> TacML CAst.(make ?loc (opn,List.map (subst_tacarg subst) l)) and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body) and subst_tacarg subst = function | Reference r -> Reference (subst_reference subst r) | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c) - | TacCall (loc,(f,l)) -> - TacCall (Loc.tag ?loc (subst_reference subst f, List.map (subst_tacarg subst) l)) + | TacCall { CAst.loc; v=(f,l) } -> + TacCall CAst.(make ?loc (subst_reference subst f, List.map (subst_tacarg subst) l)) | TacFreshId _ as x -> x | TacPretype c -> TacPretype (subst_glob_constr subst c) | TacNumgoals -> TacNumgoals diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 6bab8d0353..877d4ee758 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -365,7 +365,7 @@ let explain_ltac_call_trace last trace loc = Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" | Tacexpr.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) - (Tacexpr.TacAtom (Loc.tag te))) + (Tacexpr.TacAtom (CAst.make te))) | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) -> quote (Printer.pr_glob_constr_env (Global.env()) c) ++ (if not (Id.Map.is_empty vars) then diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 299bc7ea4d..561bfc5d7c 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -191,7 +191,7 @@ let make_unfold name = let u_not = make_unfold "not" let reduction_not_iff _ ist = - let make_reduce c = TacAtom (Loc.tag @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in + let make_reduce c = TacAtom (CAst.make @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in let tac = match !negation_unfolding with | true -> make_reduce [u_not] | false -> TacId [] @@ -244,7 +244,7 @@ let with_flags flags _ ist = let x = CAst.make @@ Id.of_string "x" in let arg = Val.Dyn (tag_tauto_flags, flags) in let ist = { ist with lfun = Id.Map.add x.CAst.v arg ist.lfun } in - eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (Locus.ArgVar f, [Reference (Locus.ArgVar x)])))) + eval_tactic_ist ist (TacArg (CAst.make @@ TacCall (CAst.make (Locus.ArgVar f, [Reference (Locus.ArgVar x)])))) let register_tauto_tactic tac name0 args = let ids = List.map (fun id -> Id.of_string id) args in @@ -252,7 +252,7 @@ let register_tauto_tactic tac name0 args = let name = { mltac_plugin = tauto_plugin; mltac_tactic = name0; } in let entry = { mltac_name = name; mltac_index = 0 } in let () = Tacenv.register_ml_tactic name [| tac |] in - let tac = TacFun (ids, TacML (Loc.tag (entry, []))) in + let tac = TacFun (ids, TacML (CAst.make (entry, []))) in let obj () = Tacenv.register_ltac true true (Id.of_string name0) tac in Mltop.declare_cache_obj obj tauto_plugin diff --git a/plugins/setoid_ring/g_newring.mlg b/plugins/setoid_ring/g_newring.mlg index 3ddea7eb30..f59ca4cef4 100644 --- a/plugins/setoid_ring/g_newring.mlg +++ b/plugins/setoid_ring/g_newring.mlg @@ -86,7 +86,7 @@ END VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] -> { let l = match l with None -> [] | Some l -> l in add_theory id t l } - | [ "Print" "Rings" ] => {Vernac_classifier.classify_as_query} -> { + | [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> { Feedback.msg_notice (strbrk "The following ring structures have been declared:"); Spmap.iter (fun fn fi -> let sigma, env = Pfedit.get_current_context () in @@ -130,7 +130,7 @@ END VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF | [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] -> { let l = match l with None -> [] | Some l -> l in add_field_theory id t l } -| [ "Print" "Fields" ] => {Vernac_classifier.classify_as_query} -> { +| [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> { Feedback.msg_notice (strbrk "The following field structures have been declared:"); Spmap.iter (fun fn fi -> let sigma, env = Pfedit.get_current_context () in diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index a2dce621d9..4109e9cf38 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -129,7 +129,7 @@ let closed_term_ast = fun l -> let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in TacFun([Name(Id.of_string"t")], - TacML(Loc.tag (tacname, + TacML(CAst.make (tacname, [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None)); TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))) (* @@ -160,7 +160,7 @@ let decl_constant na univs c = (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = - TacArg(Loc.tag @@ TacCall (Loc.tag (ArgArg(Loc.tag @@ Lazy.force tac),args))) + TacArg(CAst.make @@ TacCall (CAst.make (ArgArg(Loc.tag @@ Lazy.force tac),args))) let dummy_goal env sigma = let (gl,_,sigma) = @@ -197,7 +197,7 @@ let exec_tactic env evd n f args = (** Build the getter *) let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in - let get_res = TacML (Loc.tag (get_res, [TacGeneric n])) in + let get_res = TacML (CAst.make (get_res, [TacGeneric n])) in let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in (** Evaluate the whole result *) let gl = dummy_goal env evd in @@ -557,7 +557,7 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac = closed_term_ast (List.map Smartlocate.global_with_alias lc) | None -> let t = ArgArg(Loc.tag @@ Lazy.force ltac_inv_morph_nothing) in - TacArg(Loc.tag (TacCall(Loc.tag (t,[])))) + TacArg(CAst.make (TacCall(CAst.make (t,[])))) let make_hyp env evd c = let t = Retyping.get_type_of env !evd c in @@ -582,7 +582,7 @@ let interp_power env evdref pow = match pow with | None -> let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in - (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evdref coq_None [|carrier|]) + (TacArg(CAst.make (TacCall(CAst.make (t,[])))), plapp evdref coq_None [|carrier|]) | Some (tac, spec) -> let tac = match tac with diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index a618fc781f..3a7cf41d43 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -371,7 +371,7 @@ Ltac prop_congr := apply: prop_congr. Lemma is_true_true : true. Proof. by []. Qed. Lemma not_false_is_true : ~ false. Proof. by []. Qed. Lemma is_true_locked_true : locked true. Proof. by unlock. Qed. -Hint Resolve is_true_true not_false_is_true is_true_locked_true. +Hint Resolve is_true_true not_false_is_true is_true_locked_true : core. (** Shorter names. **) Definition isT := is_true_true. diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index ddfd4c101f..80d421b9fc 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -859,7 +859,7 @@ let ssr_n_tac seed n gl = with Not_found -> if n = -1 then fail "The ssreflect library was not loaded" else fail ("The tactic "^name^" was not found") in - let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in + let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in Proofview.V82.of_tactic (Tacinterp.eval_tactic (Tacexpr.TacArg tacexpr)) gl let donetac n gl = ssr_n_tac "done" n gl diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index e2c0ed7c8b..6535cad8b7 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -398,7 +398,7 @@ End ExtensionalEquality. Typeclasses Opaque eqfun. Typeclasses Opaque eqrel. -Hint Resolve frefl rrefl. +Hint Resolve frefl rrefl : core. Notation "f1 =1 f2" := (eqfun f1 f2) (at level 70, no associativity) : fun_scope. diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 52240f5896..7c91860228 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -1545,9 +1545,9 @@ let test_ssrseqvar = Gram.Entry.of_parser "test_ssrseqvar" accept_ssrseqvar let swaptacarg (loc, b) = (b, []), Some (TacId []) let check_seqtacarg dir arg = match snd arg, dir with - | ((true, []), Some (TacAtom (loc, _))), L2R -> + | ((true, []), Some (TacAtom { CAst.loc })), L2R -> CErrors.user_err ?loc (str "expected \"last\"") - | ((false, []), Some (TacAtom (loc, _))), R2L -> + | ((false, []), Some (TacAtom { CAst.loc })), R2L -> CErrors.user_err ?loc (str "expected \"first\"") | _, _ -> arg @@ -1677,7 +1677,7 @@ let set_pr_ssrtac name prec afmt = (* FIXME *) () (* | ArgCoq at -> Egramml.GramTerminal "COQ_ARG") afmt in let tacname = ssrtac_name name in () *) -let ssrtac_atom ?loc name args = TacML (Loc.tag ?loc (ssrtac_entry name 0, args)) +let ssrtac_atom ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name 0, args)) let ssrtac_expr ?loc name args = ssrtac_atom ?loc name args let tclintros_expr ?loc tac ipats = @@ -1704,7 +1704,7 @@ END GRAMMAR EXTEND Gram GLOBAL: tactic_expr; - ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { Loc.tag ~loc (Tacexp tac) } ]]; + ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]]; tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]]; END @@ -1724,7 +1724,7 @@ let ssrautoprop gl = let tacname = try Tacenv.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop")) with Not_found -> Tacenv.locate_tactic (ssrqid "ssrautoprop") in - let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in + let tacexpr = CAst.make @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl with Not_found -> V82.of_tactic (Auto.full_trivial []) gl diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 5dcbf9b3ef..142d1ac790 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -1388,7 +1388,7 @@ let () = let () = Tacenv.register_ml_tactic name [|mltac|] in let tac = TacFun ([Name (Id.of_string "pattern")], - TacML (Loc.tag ({ mltac_name = name; mltac_index = 0 }, []))) in + TacML (CAst.make ({ mltac_name = name; mltac_index = 0 }, []))) in let obj () = Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in Mltop.declare_cache_obj obj "ssrmatching_plugin" diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e698ba9f8f..712eb21ee6 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -71,27 +71,26 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n let print_basename sp = pr_global (ConstRef sp) let print_ref reduce ref udecl = - let typ, univs = Typeops.type_of_global_in_context (Global.env ()) ref in + let env = Global.env () in + let typ, univs = Typeops.type_of_global_in_context env ref in let inst = Univ.make_abstract_instance univs in - let bl = UnivNames.universe_binders_with_opt_names ref udecl in + let bl = UnivNames.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in let typ = EConstr.of_constr typ in let typ = if reduce then - let env = Global.env () in let ctx,ccl = Reductionops.splay_prod_assum env sigma typ in EConstr.it_mkProd_or_LetIn ccl ctx else typ in let variance = match ref with | VarRef _ | ConstRef _ -> None | IndRef (ind,_) | ConstructRef ((ind,_),_) -> - let mind = Environ.lookup_mind ind (Global.env ()) in + let mind = Environ.lookup_mind ind env in begin match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> None | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi) end in - let env = Global.env () in let inst = if Global.is_polymorphic ref then Printer.pr_universe_instance sigma inst @@ -571,7 +570,7 @@ let print_constant with_values sep sp udecl = in let ctx = UState.of_binders - (UnivNames.universe_binders_with_opt_names (ConstRef sp) udecl) + (UnivNames.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl) in let env = Global.env () and sigma = Evd.from_ctx ctx in let pr_ltype = pr_ltype_env env sigma in diff --git a/printing/printer.ml b/printing/printer.ml index dfe987a671..831008a957 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -244,8 +244,19 @@ let pr_abstract_cumulativity_info sigma cumi = let pr_global_env = Nametab.pr_global_env let pr_global = pr_global_env Id.Set.empty +let pr_universe_instance_constraints evd inst csts = + let open Univ in + let prlev = Termops.pr_evd_level evd in + let pcsts = if Constraint.is_empty csts then mt() + else str " |= " ++ + prlist_with_sep (fun () -> str "," ++ spc()) + (fun (u,d,v) -> hov 0 (prlev u ++ pr_constraint_type d ++ prlev v)) + (Constraint.elements csts) + in + str"@{" ++ Instance.pr prlev inst ++ pcsts ++ str"}" + let pr_universe_instance evd inst = - str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" + pr_universe_instance_constraints evd inst Univ.Constraint.empty let pr_puniverses f env sigma (c,u) = if !Constrextern.print_universes diff --git a/printing/printer.mli b/printing/printer.mli index cfa1caef00..785f452a7b 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -85,6 +85,7 @@ val pr_sort : evar_map -> Sorts.t -> Pp.t val pr_polymorphic : bool -> Pp.t val pr_cumulative : bool -> bool -> Pp.t val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t +val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Constraint.t -> Pp.t val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> Univ.UContext.t -> Pp.t val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> diff --git a/printing/printmod.ml b/printing/printmod.ml index cc40c74998..2c3ab46670 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -119,7 +119,9 @@ let print_mutual_inductive env mind mib udecl = | BiFinite -> "Variant" | CoFinite -> "CoInductive" in - let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) udecl in + let bl = UnivNames.universe_binders_with_opt_names + (Declareops.inductive_polymorphic_context mib) udecl + in let sigma = Evd.from_ctx (UState.of_binders bl) in hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ Printer.pr_cumulative @@ -157,7 +159,9 @@ let print_record env mind mib udecl = let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in - let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0)) udecl in + let bl = UnivNames.universe_binders_with_opt_names (Declareops.inductive_polymorphic_context mib) + udecl + in let sigma = Evd.from_ctx (UState.of_binders bl) in let keyword = let open Declarations in @@ -296,7 +300,7 @@ let print_body is_impl extent env mp (l,body) = (match extent with | OnlyNames -> mt () | WithContents -> - let bl = UnivNames.universe_binders_with_opt_names (ConstRef (Constant.make2 mp l)) None in + let bl = UnivNames.universe_binders_with_opt_names ctx None in let sigma = Evd.from_ctx (UState.of_binders bl) in str " :" ++ spc () ++ hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++ diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 7b55941874..78080fa203 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -35,16 +35,6 @@ let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator = | None -> p,(true,[]) | Some tac -> Proof.run_tactic env tac p)) -let cook_this_proof p = - match p with - | { Proof_global.id;entries=[constr];persistence;universes } -> - (id,(constr,universes,persistence)) - | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.") - -let cook_proof () = - cook_this_proof (fst - (Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x))) - exception NoSuchGoal let _ = CErrors.register_handler begin function | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") @@ -155,10 +145,15 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo start_proof id goal_kind evd sign typ terminator; try let status = by tac in - let _,(const,univs,_) = cook_proof () in - Proof_global.discard_current (); - let univs = UState.demote_seff_univs const univs in - const, status, univs + let open Proof_global in + let { entries; universes } = fst @@ close_proof ~keep_body_ucst_separate:false (fun x -> x) in + match entries with + | [entry] -> + discard_current (); + let univs = UState.demote_seff_univs entry universes in + entry, status, univs + | _ -> + CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") with reraise -> let reraise = CErrors.push reraise in Proof_global.discard_current (); diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 50ce267c81..76be7936b4 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -29,21 +29,6 @@ val start_proof : Proof_global.proof_terminator -> unit (** {6 ... } *) -(** [cook_proof opacity] turns the current proof (assumed completed) into - a constant with its name, kind and possible hook (see [start_proof]); - it fails if there is no current proof of if it is not completed; - it also tells if the guardness condition has to be inferred. *) - -val cook_this_proof : - Proof_global.proof_object -> - (Id.t * - (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind)) - -val cook_proof : unit -> - (Id.t * - (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind)) - -(** {6 ... } *) (** [get_goal_context n] returns the context of the [n]th subgoal of the current focused proof or raises a [UserError] if there is no focused proof or if there is no more subgoals *) diff --git a/stm/stm.ml b/stm/stm.ml index b474bd502a..9359ab15e2 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -25,6 +25,7 @@ open CErrors open Names open Feedback open Vernacexpr +open Vernacextend module AsyncOpts = struct @@ -162,7 +163,7 @@ type branch_type = [ `Master | `Proof of proof_mode * depth | `Edit of - proof_mode * Stateid.t * Stateid.t * vernac_qed_type * Vcs_.Branch.t ] + proof_mode * Stateid.t * Stateid.t * Vernacextend.vernac_qed_type * Vcs_.Branch.t ] (* TODO 8.7 : split commands and tactics, since this type is too messy now *) type cmd_t = { ctac : bool; (* is a tactic *) @@ -174,7 +175,7 @@ type cmd_t = { | `TacQueue of solving_tac * anon_abstracting_tac * AsyncTaskQueue.cancel_switch | `QueryQueue of AsyncTaskQueue.cancel_switch | `SkipQueue ] } -type fork_t = aast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Names.Id.t list +type fork_t = aast * Vcs_.Branch.t * opacity_guarantee * Names.Id.t list type qed_t = { qast : aast; keep : vernac_qed_type; diff --git a/stm/stm.mli b/stm/stm.mli index 95117f04f4..0c0e19ce5c 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -258,7 +258,7 @@ type dynamic_block_error_recovery = doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ] val register_proof_block_delimiter : - Vernacexpr.proof_block_name -> + Vernacextend.proof_block_name -> static_block_detection -> dynamic_block_error_recovery -> unit diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 4db86817c9..526858bd73 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -12,6 +12,7 @@ open CErrors open Util open Pp open CAst +open Vernacextend open Vernacexpr let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] @@ -209,7 +210,3 @@ let classify_vernac e = | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) in static_control_classifier e - -let classify_as_query = VtQuery, VtLater -let classify_as_sideeff = VtSideff [], VtLater -let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index e82b191418..9d93ad1f39 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -8,16 +8,12 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Vernacexpr +open Vernacextend val string_of_vernac_classification : vernac_classification -> string (** What does a vernacular do *) -val classify_vernac : vernac_control -> vernac_classification - -(** Standard constant classifiers *) -val classify_as_query : vernac_classification -val classify_as_sideeff : vernac_classification -val classify_as_proofstep : vernac_classification +val classify_vernac : Vernacexpr.vernac_control -> vernac_classification +(** *) val stm_allow_nested_proofs_option_name : string list diff --git a/tactics/hints.ml b/tactics/hints.ml index 6aa021543d..e64e08dbde 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1377,10 +1377,10 @@ let interp_hints poly = let _, tacexp = Genintern.generic_intern env tacexp in HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp) -let add_hints ~local dbnames0 h = - if String.List.mem "nocore" dbnames0 then +let add_hints ~local dbnames h = + if String.List.mem "nocore" dbnames then user_err Pp.(str "The hint database \"nocore\" is meant to stay empty."); - let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in + assert (not (List.is_empty dbnames)); let env = Global.env() in let sigma = Evd.from_env env in match h with diff --git a/test-suite/bugs/closed/bug_2001.v b/test-suite/bugs/closed/bug_2001.v index 652c65706a..31c62b7b36 100644 --- a/test-suite/bugs/closed/bug_2001.v +++ b/test-suite/bugs/closed/bug_2001.v @@ -1,12 +1,10 @@ (* Automatic computing of guard in "Theorem with"; check that guard is not computed when the user explicitly indicated it *) -Unset Automatic Introduction. - Inductive T : Set := | v : T. -Definition f (s:nat) (t:T) : nat. +Definition f : forall (s:nat) (t:T), nat. fix f 2. intros s t. refine diff --git a/test-suite/bugs/closed/bug_6661.v b/test-suite/bugs/closed/bug_6661.v index e88a3704d8..28a9ffc7bd 100644 --- a/test-suite/bugs/closed/bug_6661.v +++ b/test-suite/bugs/closed/bug_6661.v @@ -53,8 +53,6 @@ Definition foo (X:Type) (xy : @total2 X (λ _, X)) : X. exact x. Defined. -Unset Automatic Introduction. - Definition idfun (T : UU) := λ t:T, t. Definition pathscomp0 {X : UU} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index d63b6dbfce..4d3f7419e6 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -41,8 +41,7 @@ Arguments A, Wrap are implicit and maximally inserted Argument scopes are [type_scope _] Polymorphic bar@{u} = nat : Wrap@{u} Set -(* u |= Set < u - *) +(* u |= Set < u *) bar is universe polymorphic Polymorphic foo@{u UnivBinders.17 v} = diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index efb32ef6f7..81c9763ccd 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -50,8 +50,6 @@ End folding. (* Check definition by tactics *) -Set Automatic Introduction. - Inductive even : nat -> Type := | even_O : even 0 | even_S : forall n, odd n -> even (S n) diff --git a/test-suite/success/Require.v b/test-suite/success/Require.v index f851d8c7d9..de5987c4f7 100644 --- a/test-suite/success/Require.v +++ b/test-suite/success/Require.v @@ -1,3 +1,8 @@ +(* -*- coq-prog-args: ("-noinit"); -*- *) + Require Import Coq.Arith.Plus. Require Coq.Arith.Minus. Locate Library Coq.Arith.Minus. + +(* Check that Init didn't get exported by the import above *) +Fail Check nat. diff --git a/test-suite/success/autointros.v b/test-suite/success/autointros.v index 0a0812711c..1140a537fc 100644 --- a/test-suite/success/autointros.v +++ b/test-suite/success/autointros.v @@ -1,5 +1,3 @@ -Set Automatic Introduction. - Inductive even : nat -> Prop := | even_0 : even 0 | even_odd : forall n, odd n -> even (S n) diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 42af3583d4..075288e216 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -48,7 +48,7 @@ Proof. discriminate. Qed. Hint Resolve diff_false_true : bool. -Hint Extern 1 (false <> true) => exact diff_false_true. +Hint Extern 1 (false <> true) => exact diff_false_true : core. Lemma eq_true_false_abs : forall b:bool, b = true -> b = false -> False. Proof. @@ -621,7 +621,7 @@ Lemma absurd_eq_true : forall b, False -> b = true. Proof. contradiction. Qed. -Hint Resolve absurd_eq_true. +Hint Resolve absurd_eq_true : core. (* A specific instance of eq_trans that preserves compatibility with old hint bool_2 *) @@ -630,7 +630,7 @@ Lemma trans_eq_bool : forall x y z:bool, x = y -> y = z -> x = z. Proof. apply eq_trans. Qed. -Hint Resolve trans_eq_bool. +Hint Resolve trans_eq_bool : core. (*****************************************) (** * Reflection of [bool] into [Prop] *) diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index 7af2b0fc45..3e6358c8f3 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -157,6 +157,6 @@ Section RelProd_Instances. Proof. unfold RelCompFun; firstorder. Qed. End RelProd_Instances. -Hint Unfold RelProd RelCompFun. -Hint Extern 2 (RelProd _ _ _ _) => split. +Hint Unfold RelProd RelCompFun : core. +Hint Extern 2 (RelProd _ _ _ _) => split : core. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index b0d1824827..8fc04d81e6 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -41,7 +41,7 @@ Local Open Scope Int_scope. Local Notation int := I.t. Definition key := X.t. -Hint Transparent key. +Hint Transparent key : core. (** * Trees *) @@ -488,8 +488,8 @@ Functional Scheme map2_opt_ind := Induction for map2_opt Sort Prop. (** * Automation and dedicated tactics. *) -Hint Constructors tree MapsTo In bst. -Hint Unfold lt_tree gt_tree. +Hint Constructors tree MapsTo In bst : core. +Hint Unfold lt_tree gt_tree : core. Tactic Notation "factornode" ident(l) ident(x) ident(d) ident(r) ident(h) "as" ident(s) := @@ -569,7 +569,7 @@ Lemma MapsTo_In : forall k e m, MapsTo k e m -> In k m. Proof. induction 1; auto. Qed. -Hint Resolve MapsTo_In. +Hint Resolve MapsTo_In : core. Lemma In_MapsTo : forall k m, In k m -> exists e, MapsTo k e m. Proof. @@ -588,7 +588,7 @@ Lemma MapsTo_1 : Proof. induction m; simpl; intuition_in; eauto. Qed. -Hint Immediate MapsTo_1. +Hint Immediate MapsTo_1 : core. Lemma In_1 : forall m x y, X.eq x y -> In x m -> In y m. @@ -627,7 +627,7 @@ Proof. unfold gt_tree in *; intuition_in; order. Qed. -Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node. +Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core. Lemma lt_left : forall x y l r e h, lt_tree x (Node l y e r h) -> lt_tree x l. @@ -653,7 +653,7 @@ Proof. intuition_in. Qed. -Hint Resolve lt_left lt_right gt_left gt_right. +Hint Resolve lt_left lt_right gt_left gt_right : core. Lemma lt_tree_not_in : forall x m, lt_tree x m -> ~ In x m. @@ -679,7 +679,7 @@ Proof. eauto. Qed. -Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans. +Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core. (** * Empty map *) @@ -811,7 +811,7 @@ Lemma create_bst : Proof. unfold create; auto. Qed. -Hint Resolve create_bst. +Hint Resolve create_bst : core. Lemma create_in : forall l x e r y, @@ -828,7 +828,7 @@ Proof. (apply lt_tree_node || apply gt_tree_node); auto; (eapply lt_tree_trans || eapply gt_tree_trans); eauto. Qed. -Hint Resolve bal_bst. +Hint Resolve bal_bst : core. Lemma bal_in : forall l x e r y, In y (bal l x e r) <-> X.eq y x \/ In y l \/ In y r. @@ -869,7 +869,7 @@ Proof. apply MX.eq_lt with x; auto. apply MX.lt_eq with x; auto. Qed. -Hint Resolve add_bst. +Hint Resolve add_bst : core. Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m). Proof. @@ -949,7 +949,7 @@ Proof. destruct 1. apply H2; intuition. Qed. -Hint Resolve remove_min_bst. +Hint Resolve remove_min_bst : core. Lemma remove_min_gt_tree : forall l x e r h, bst (Node l x e r h) -> @@ -968,7 +968,7 @@ Proof. assert (X.lt m#1 x) by order. decompose [or] H; order. Qed. -Hint Resolve remove_min_gt_tree. +Hint Resolve remove_min_gt_tree : core. Lemma remove_min_find : forall l x e r h y, bst (Node l x e r h) -> @@ -1120,7 +1120,7 @@ Proof. intuition; [ apply MX.lt_eq with x | ]; eauto. intuition; [ apply MX.eq_lt with x | ]; eauto. Qed. -Hint Resolve join_bst. +Hint Resolve join_bst : core. Lemma join_find : forall l x d r y, bst l -> bst r -> lt_tree x l -> gt_tree x r -> @@ -1256,7 +1256,7 @@ Proof. rewrite remove_min_in, e1; simpl; auto. change (gt_tree (m2',xd)#2#1 (m2',xd)#1). rewrite <-e1; eauto. Qed. -Hint Resolve concat_bst. +Hint Resolve concat_bst : core. Lemma concat_find : forall m1 m2 y, bst m1 -> bst m2 -> (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) -> @@ -1344,7 +1344,7 @@ Proof. intros; unfold elements; apply elements_aux_sort; auto. intros; inversion H0. Qed. -Hint Resolve elements_sort. +Hint Resolve elements_sort : core. Lemma elements_nodup : forall s : t elt, bst s -> NoDupA eqk (elements s). Proof. @@ -1612,7 +1612,7 @@ destruct (map_option_2 H) as (d0 & ? & ?). destruct (map_option_2 H') as (d0' & ? & ?). eapply X.lt_trans with x; eauto using MapsTo_In. Qed. -Hint Resolve map_option_bst. +Hint Resolve map_option_bst : core. Ltac nonify e := replace e with (@None elt) by @@ -1711,7 +1711,7 @@ apply X.lt_trans with x1. destruct (map2_opt_2 H1 H6 Hy); intuition. destruct (map2_opt_2 H2 H7 Hy'); intuition. Qed. -Hint Resolve map2_opt_bst. +Hint Resolve map2_opt_bst : core. Ltac map2_aux := match goal with @@ -2066,7 +2066,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Proof. destruct c; simpl; intros; P.MX.elim_comp; auto. Qed. - Hint Resolve cons_Cmp. + Hint Resolve cons_Cmp : core. Lemma compare_end_Cmp : forall e2, Cmp (compare_end e2) nil (P.flatten_e e2). diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 2d5a79838a..d19c5558d8 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -20,7 +20,7 @@ Require Export FMapInterface. Set Implicit Arguments. Unset Strict Implicit. -Hint Extern 1 (Equivalence _) => constructor; congruence. +Hint Extern 1 (Equivalence _) => constructor; congruence : core. (** * Facts about weak maps *) diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index c0db8646c7..950b30ee4d 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -63,7 +63,7 @@ Inductive avl : t elt -> Prop := (** * Automation and dedicated tactics about [avl]. *) -Hint Constructors avl. +Hint Constructors avl : core. Lemma height_non_negative : forall (s : t elt), avl s -> height s >= 0. @@ -100,7 +100,7 @@ Lemma avl_node : forall x e l r, avl l -> avl r -> Proof. intros; auto. Qed. -Hint Resolve avl_node. +Hint Resolve avl_node : core. (** Results about [height] *) @@ -193,7 +193,7 @@ Lemma add_avl : forall m x e, avl m -> avl (add x e m). Proof. intros; generalize (add_avl_1 x e H); intuition. Qed. -Hint Resolve add_avl. +Hint Resolve add_avl : core. (** * Extraction of minimum binding *) @@ -274,7 +274,7 @@ Lemma remove_avl : forall m x, avl m -> avl (remove x m). Proof. intros; generalize (remove_avl_1 x H); intuition. Qed. -Hint Resolve remove_avl. +Hint Resolve remove_avl : core. (** * Join *) @@ -331,7 +331,7 @@ Lemma join_avl : forall l x d r, avl l -> avl r -> avl (join l x d r). Proof. intros; destruct (join_avl_1 x d H H0); auto. Qed. -Hint Resolve join_avl. +Hint Resolve join_avl : core. (** concat *) @@ -341,7 +341,7 @@ Proof. intros; apply join_avl; auto. generalize (remove_min_avl H0); rewrite e1; simpl; auto. Qed. -Hint Resolve concat_avl. +Hint Resolve concat_avl : core. (** split *) @@ -355,7 +355,7 @@ Proof. Qed. End Elt. -Hint Constructors avl. +Hint Constructors avl : core. Section Map. Variable elt elt' : Type. @@ -713,7 +713,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Proof. destruct c; simpl; intros; MX.elim_comp; auto. Qed. - Hint Resolve cons_Cmp. + Hint Resolve cons_Cmp : core. Lemma compare_aux_Cmp : forall e, Cmp (compare_aux e) (flatten_e (fst e)) (flatten_e (snd e)). diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v index 38a96dc393..8970529103 100644 --- a/theories/FSets/FMapInterface.v +++ b/theories/FSets/FMapInterface.v @@ -58,7 +58,7 @@ Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true. Module Type WSfun (E : DecidableType). Definition key := E.t. - Hint Transparent key. + Hint Transparent key : core. Parameter t : Type -> Type. (** the abstract type of maps *) diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 3e98d11976..6ca158a277 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -51,7 +51,7 @@ Proof. intro abs. inversion abs. Qed. -Hint Resolve empty_1. +Hint Resolve empty_1 : core. Lemma empty_sorted : Sort empty. Proof. @@ -216,7 +216,7 @@ Proof. compute in H0,H1. simpl; case (X.compare x x''); intuition. Qed. -Hint Resolve add_Inf. +Hint Resolve add_Inf : core. Lemma add_sorted : forall m (Hm:Sort m) x e, Sort (add x e m). Proof. @@ -302,7 +302,7 @@ Proof. inversion_clear Hm. apply Inf_lt with (x'',e''); auto. Qed. -Hint Resolve remove_Inf. +Hint Resolve remove_Inf : core. Lemma remove_sorted : forall m (Hm:Sort m) x, Sort (remove x m). Proof. @@ -586,7 +586,7 @@ Proof. inversion_clear H; auto. Qed. -Hint Resolve map_lelistA. +Hint Resolve map_lelistA : core. Lemma map_sorted : forall (m: t elt)(Hm : sort (@ltk elt) m)(f:elt -> elt'), sort (@ltk elt') (map f m). @@ -654,7 +654,7 @@ Proof. inversion_clear H; auto. Qed. -Hint Resolve mapi_lelistA. +Hint Resolve mapi_lelistA : core. Lemma mapi_sorted : forall m (Hm : sort (@ltk elt) m)(f: key ->elt -> elt'), sort (@ltk elt') (mapi f m). @@ -781,7 +781,7 @@ Proof. inversion_clear H; auto. inversion_clear H0; auto. Qed. -Hint Resolve combine_lelistA. +Hint Resolve combine_lelistA : core. Lemma combine_sorted : forall m (Hm : sort (@ltk elt) m) m' (Hm' : sort (@ltk elt') m'), diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 6736096509..03dce9666d 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -49,7 +49,7 @@ Proof. inversion abs. Qed. -Hint Resolve empty_1. +Hint Resolve empty_1 : core. Lemma empty_NoDup : NoDupA empty. Proof. @@ -621,7 +621,7 @@ Proof. inversion_clear 1. intros; apply add_NoDup; auto. Qed. -Hint Resolve fold_right_pair_NoDup. +Hint Resolve fold_right_pair_NoDup : core. Lemma combine_NoDup : forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m'), diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 0c4ecb1f31..3952c28061 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -137,7 +137,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. generalize (E.eq_sym H0); case (Pdec x); case (Pdec y); firstorder. Qed. - Hint Resolve compat_P_aux. + Hint Resolve compat_P_aux : core. Definition filter : forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}) (s : t), @@ -467,7 +467,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Proof. intros; unfold elements; case (M.elements s); firstorder. Qed. - Hint Resolve elements_3. + Hint Resolve elements_3 : core. Lemma elements_3w : forall s : t, NoDupA E.eq (elements s). Proof. auto. Qed. @@ -666,7 +666,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. rewrite <- H1; firstorder. Qed. - Hint Resolve compat_P_aux. + Hint Resolve compat_P_aux : core. Definition filter (f : elt -> bool) (s : t) : t := let (s', _) := filter (P:=fun x => f x = true) (f_dec f) s in s'. diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v index 0926d3ae9f..fa7f1c5f4e 100644 --- a/theories/FSets/FSetInterface.v +++ b/theories/FSets/FSetInterface.v @@ -253,7 +253,7 @@ Module Type WSfun (E : DecidableType). End Spec. - Hint Transparent elt. + Hint Transparent elt : core. Hint Resolve mem_1 equal_1 subset_1 empty_1 is_empty_1 choose_1 choose_2 add_1 add_2 remove_1 remove_2 singleton_2 union_1 union_2 union_3 diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index c9cfb94ace..17f0e25e7a 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -21,8 +21,8 @@ Require Import DecidableTypeEx FSetFacts FSetDecide. Set Implicit Arguments. Unset Strict Implicit. -Hint Unfold transpose compat_op Proper respectful. -Hint Extern 1 (Equivalence _) => constructor; congruence. +Hint Unfold transpose compat_op Proper respectful : core. +Hint Extern 1 (Equivalence _) => constructor; congruence : core. (** First, a functor for Weak Sets in functorial version. *) @@ -732,7 +732,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). Proof. intros; rewrite cardinal_Empty; auto. Qed. - Hint Resolve cardinal_inv_1. + Hint Resolve cardinal_inv_1 : core. Lemma cardinal_inv_2 : forall s n, cardinal s = S n -> { x : elt | In x s }. @@ -769,7 +769,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). exact Equal_cardinal. Qed. - Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal. + Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : core. (** ** Cardinal and set operators *) @@ -887,7 +887,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). auto with set. Qed. - Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2. + Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : core. End WProperties_fun. @@ -952,7 +952,7 @@ Module OrdProperties (M:S). red; intros x a b H; unfold leb. f_equal; apply gtb_compat; auto. Qed. - Hint Resolve gtb_compat leb_compat. + Hint Resolve gtb_compat leb_compat : core. Lemma elements_split : forall x s, elements s = elements_lt x s ++ elements_ge x s. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 75f14bb4da..7f0387dd12 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -136,7 +136,7 @@ Defined. Inductive BoolSpec (P Q : Prop) : bool -> Prop := | BoolSpecT : P -> BoolSpec P Q true | BoolSpecF : Q -> BoolSpec P Q false. -Hint Constructors BoolSpec. +Hint Constructors BoolSpec : core. (********************************************************************) @@ -344,7 +344,7 @@ Inductive CompareSpec (Peq Plt Pgt : Prop) : comparison -> Prop := | CompEq : Peq -> CompareSpec Peq Plt Pgt Eq | CompLt : Plt -> CompareSpec Peq Plt Pgt Lt | CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt. -Hint Constructors CompareSpec. +Hint Constructors CompareSpec : core. (** For having clean interfaces after extraction, [CompareSpec] is declared in Prop. For some situations, it is nonetheless useful to have a @@ -354,7 +354,7 @@ Inductive CompareSpecT (Peq Plt Pgt : Prop) : comparison -> Type := | CompEqT : Peq -> CompareSpecT Peq Plt Pgt Eq | CompLtT : Plt -> CompareSpecT Peq Plt Pgt Lt | CompGtT : Pgt -> CompareSpecT Peq Plt Pgt Gt. -Hint Constructors CompareSpecT. +Hint Constructors CompareSpecT : core. Lemma CompareSpec2Type : forall Peq Plt Pgt c, CompareSpec Peq Plt Pgt c -> CompareSpecT Peq Plt Pgt c. @@ -371,7 +371,7 @@ Definition CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop := Definition CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type := CompareSpecT (eq x y) (lt x y) (lt y x). -Hint Unfold CompSpec CompSpecT. +Hint Unfold CompSpec CompSpecT : core. Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c, CompSpec eq lt x y c -> CompSpecT eq lt x y c. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 4614d215eb..d5241e622c 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -219,7 +219,7 @@ Section Facts. Proof. auto using app_assoc. Qed. - Hint Resolve app_assoc_reverse. + Hint Resolve app_assoc_reverse : core. (* end hide *) (** [app] commutes with [cons] *) @@ -1569,19 +1569,19 @@ Section SetIncl. Variable A : Type. Definition incl (l m:list A) := forall a:A, In a l -> In a m. - Hint Unfold incl. + Hint Unfold incl : core. Lemma incl_refl : forall l:list A, incl l l. Proof. auto. Qed. - Hint Resolve incl_refl. + Hint Resolve incl_refl : core. Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m). Proof. auto with datatypes. Qed. - Hint Immediate incl_tl. + Hint Immediate incl_tl : core. Lemma incl_tran : forall l m n:list A, incl l m -> incl m n -> incl l n. Proof. @@ -1592,13 +1592,13 @@ Section SetIncl. Proof. auto with datatypes. Qed. - Hint Immediate incl_appl. + Hint Immediate incl_appl : core. Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n). Proof. auto with datatypes. Qed. - Hint Immediate incl_appr. + Hint Immediate incl_appr : core. Lemma incl_cons : forall (a:A) (l m:list A), In a m -> incl l m -> incl (a :: l) m. @@ -1613,7 +1613,7 @@ Section SetIncl. now_show (In a0 l -> In a0 m). auto. Qed. - Hint Resolve incl_cons. + Hint Resolve incl_cons : core. Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n. Proof. @@ -1621,7 +1621,7 @@ Section SetIncl. now_show (In a n). elim (in_app_or _ _ _ H1); auto. Qed. - Hint Resolve incl_app. + Hint Resolve incl_app : core. End SetIncl. @@ -2180,7 +2180,7 @@ Section Exists_Forall. | Exists_cons_hd : forall x l, P x -> Exists (x::l) | Exists_cons_tl : forall x l, Exists l -> Exists (x::l). - Hint Constructors Exists. + Hint Constructors Exists : core. Lemma Exists_exists (l:list A) : Exists l <-> (exists x, In x l /\ P x). @@ -2214,7 +2214,7 @@ Section Exists_Forall. | Forall_nil : Forall nil | Forall_cons : forall x l, P x -> Forall l -> Forall (x::l). - Hint Constructors Forall. + Hint Constructors Forall : core. Lemma Forall_forall (l:list A): Forall l <-> (forall x, In x l -> P x). @@ -2299,8 +2299,8 @@ Section Exists_Forall. End Exists_Forall. -Hint Constructors Exists. -Hint Constructors Forall. +Hint Constructors Exists : core. +Hint Constructors Forall : core. Section Forall2. @@ -2314,7 +2314,7 @@ Section Forall2. | Forall2_cons : forall x y l l', R x y -> Forall2 l l' -> Forall2 (x::l) (y::l'). - Hint Constructors Forall2. + Hint Constructors Forall2 : core. Theorem Forall2_refl : Forall2 [] []. Proof. intros; apply Forall2_nil. Qed. @@ -2348,7 +2348,7 @@ Section Forall2. Qed. End Forall2. -Hint Constructors Forall2. +Hint Constructors Forall2 : core. Section ForallPairs. @@ -2369,7 +2369,7 @@ Section ForallPairs. | FOP_cons : forall a l, Forall (R a) l -> ForallOrdPairs l -> ForallOrdPairs (a::l). - Hint Constructors ForallOrdPairs. + Hint Constructors ForallOrdPairs : core. Lemma ForallOrdPairs_In : forall l, ForallOrdPairs l -> diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index cc7d6f5536..3afdd8df27 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -193,7 +193,7 @@ Section first_definitions. | auto with datatypes ]. Qed. - Hint Resolve set_add_intro1 set_add_intro2. + Hint Resolve set_add_intro1 set_add_intro2 : core. Lemma set_add_intro : forall (a b:A) (x:set), a = b \/ set_In a x -> set_In a (set_add b x). @@ -224,7 +224,7 @@ Section first_definitions. case H1; trivial. Qed. - Hint Resolve set_add_intro set_add_elim set_add_elim2. + Hint Resolve set_add_intro set_add_elim set_add_elim2 : core. Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set. Proof. @@ -310,7 +310,7 @@ Section first_definitions. intros; elim H0; auto with datatypes. Qed. - Hint Resolve set_union_intro2 set_union_intro1. + Hint Resolve set_union_intro2 set_union_intro1 : core. Lemma set_union_intro : forall (a:A) (x y:set), @@ -393,7 +393,7 @@ Section first_definitions. eauto with datatypes. Qed. - Hint Resolve set_inter_elim1 set_inter_elim2. + Hint Resolve set_inter_elim1 set_inter_elim2 : core. Lemma set_inter_elim : forall (a:A) (x y:set), @@ -471,7 +471,7 @@ Section first_definitions. apply (set_diff_elim1 _ _ _ H). Qed. -Hint Resolve set_diff_intro set_diff_trivial. +Hint Resolve set_diff_intro set_diff_trivial : core. End first_definitions. diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 0c5fe55b27..cab4c23df1 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -30,7 +30,7 @@ Inductive InA (x : A) : list A -> Prop := | InA_cons_hd : forall y l, eqA x y -> InA x (y :: l) | InA_cons_tl : forall y l, InA x l -> InA x (y :: l). -Hint Constructors InA. +Hint Constructors InA : core. (** TODO: it would be nice to have a generic definition instead of the previous one. Having [InA = Exists eqA] raises too @@ -62,7 +62,7 @@ Inductive NoDupA : list A -> Prop := | NoDupA_nil : NoDupA nil | NoDupA_cons : forall x l, ~ InA x l -> NoDupA l -> NoDupA (x::l). -Hint Constructors NoDupA. +Hint Constructors NoDupA : core. (** An alternative definition of [NoDupA] based on [ForallOrdPairs] *) @@ -93,7 +93,7 @@ Inductive eqlistA : list A -> list A -> Prop := | eqlistA_cons : forall x x' l l', eqA x x' -> eqlistA l l' -> eqlistA (x::l) (x'::l'). -Hint Constructors eqlistA. +Hint Constructors eqlistA : core. (** We could also have written [eqlistA = Forall2 eqA]. *) @@ -107,8 +107,8 @@ Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv). Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv). Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv). -Hint Resolve eqarefl eqatrans. -Hint Immediate eqasym. +Hint Resolve eqarefl eqatrans : core. +Hint Immediate eqasym : core. Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA. @@ -154,14 +154,14 @@ Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l. Proof. intros l x y H H'. rewrite <- H. auto. Qed. -Hint Immediate InA_eqA. +Hint Immediate InA_eqA : core. Lemma In_InA : forall l x, In x l -> InA x l. Proof. simple induction l; simpl; intuition. subst; auto. Qed. -Hint Resolve In_InA. +Hint Resolve In_InA : core. Lemma InA_split : forall l x, InA x l -> exists l1 y l2, eqA x y /\ l = l1++y::l2. @@ -786,12 +786,12 @@ Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA. Let sotrans := (@StrictOrder_Transitive _ _ ltA_strorder). -Hint Resolve sotrans. +Hint Resolve sotrans : core. Notation InfA:=(lelistA ltA). Notation SortA:=(sort ltA). -Hint Constructors lelistA sort. +Hint Constructors lelistA sort : core. Lemma InfA_ltA : forall l x y, ltA x y -> InfA y l -> InfA x l. @@ -814,7 +814,7 @@ Lemma InfA_eqA l x y : eqA x y -> InfA y l -> InfA x l. Proof using eqA_equiv ltA_compat. intros H; now rewrite H. Qed. -Hint Immediate InfA_ltA InfA_eqA. +Hint Immediate InfA_ltA InfA_eqA : core. Lemma SortA_InfA_InA : forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x. @@ -1005,7 +1005,7 @@ Qed. End Filter. End Type_with_equality. -Hint Constructors InA eqlistA NoDupA sort lelistA. +Hint Constructors InA eqlistA NoDupA sort lelistA : core. Arguments equivlistA_cons_nil {A} eqA {eqA_equiv} x l _. Arguments equivlistA_nil_eq {A} eqA {eqA_equiv} l _. diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v index 24b96514fd..f5ea303343 100644 --- a/theories/Lists/SetoidPermutation.v +++ b/theories/Lists/SetoidPermutation.v @@ -28,7 +28,7 @@ Inductive PermutationA : list A -> list A -> Prop := | permA_swap x y l : PermutationA (y :: x :: l) (x :: y :: l) | permA_trans l₁ l₂ l₃ : PermutationA l₁ l₂ -> PermutationA l₂ l₃ -> PermutationA l₁ l₃. -Local Hint Constructors PermutationA. +Local Hint Constructors PermutationA : core. Global Instance: Equivalence PermutationA. Proof. diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 25b7811417..3914f44a2c 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -31,7 +31,7 @@ Arguments JMeq_refl {A x} , [A] x. Register JMeq as core.JMeq.type. Register JMeq_refl as core.JMeq.refl. -Hint Resolve JMeq_refl. +Hint Resolve JMeq_refl : core. Definition JMeq_hom {A : Type} (x y : A) := JMeq x y. @@ -42,7 +42,7 @@ Proof. intros; destruct H; trivial. Qed. -Hint Immediate JMeq_sym. +Hint Immediate JMeq_sym : core. Register JMeq_sym as core.JMeq.sym. diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index aec88f93bf..ac2a143472 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -305,13 +305,13 @@ Include MSetGenTree.Props X I. (** Automation and dedicated tactics *) -Local Hint Immediate MX.eq_sym. -Local Hint Unfold In lt_tree gt_tree Ok. -Local Hint Constructors InT bst. -Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok. -Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node. -Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans. -Local Hint Resolve elements_spec2. +Local Hint Immediate MX.eq_sym : core. +Local Hint Unfold In lt_tree gt_tree Ok : core. +Local Hint Constructors InT bst : core. +Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok : core. +Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core. +Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core. +Local Hint Resolve elements_spec2 : core. (* Sometimes functional induction will expose too much of a tree structure. The following tactic allows factoring back @@ -496,7 +496,7 @@ Proof. specialize (L m); rewrite remove_min_spec, e0 in L; simpl in L; [setoid_replace y with x|inv]; eauto. Qed. -Local Hint Resolve remove_min_gt_tree. +Local Hint Resolve remove_min_gt_tree : core. (** ** Merging two trees *) diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 95868861fa..888f9850c1 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -46,7 +46,7 @@ End InfoTyp. Module Type Ops (X:OrderedType)(Info:InfoTyp). Definition elt := X.t. -Hint Transparent elt. +Hint Transparent elt : core. Inductive tree : Type := | Leaf : tree @@ -342,11 +342,11 @@ Module Import MX := OrderedTypeFacts X. Scheme tree_ind := Induction for tree Sort Prop. Scheme bst_ind := Induction for bst Sort Prop. -Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok. -Local Hint Immediate MX.eq_sym. -Local Hint Unfold In lt_tree gt_tree. -Local Hint Constructors InT bst. -Local Hint Unfold Ok. +Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok : core. +Local Hint Immediate MX.eq_sym : core. +Local Hint Unfold In lt_tree gt_tree : core. +Local Hint Constructors InT bst : core. +Local Hint Unfold Ok : core. (** Automatic treatment of [Ok] hypothesis *) @@ -432,7 +432,7 @@ Lemma In_1 : Proof. induction s; simpl; intuition_in; eauto. Qed. -Local Hint Immediate In_1. +Local Hint Immediate In_1 : core. Instance In_compat : Proper (X.eq==>eq==>iff) InT. Proof. @@ -478,7 +478,7 @@ Proof. unfold gt_tree; intuition_in; order. Qed. -Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node. +Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core. Lemma lt_tree_not_in : forall (x : elt) (t : tree), lt_tree x t -> ~ InT x t. @@ -516,7 +516,7 @@ Proof. intros x x' Hx s s' Hs H y Hy. subst. setoid_rewrite <- Hx; auto. Qed. -Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans. +Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core. Ltac induct s x := induction s as [|i l IHl x' r IHr]; simpl; intros; @@ -699,7 +699,7 @@ Proof. intros; unfold elements; apply elements_spec2'; auto. intros; inversion H0. Qed. -Local Hint Resolve elements_spec2. +Local Hint Resolve elements_spec2 : core. Lemma elements_spec2w : forall s `(Ok s), NoDupA X.eq (elements s). Proof. @@ -1035,7 +1035,7 @@ Qed. Definition Cmp c x y := CompSpec L.eq L.lt x y c. -Local Hint Unfold Cmp flip. +Local Hint Unfold Cmp flip : core. Lemma compare_end_Cmp : forall e2, Cmp (compare_end e2) nil (flatten_e e2). diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index f0e757157d..a4bbaef52d 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -884,10 +884,10 @@ Module MakeListOrdering (O:OrderedType). O.lt x y -> lt_list (x :: s) (y :: s') | lt_cons_eq : forall x y s s', O.eq x y -> lt_list s s' -> lt_list (x :: s) (y :: s'). - Hint Constructors lt_list. + Hint Constructors lt_list : core. Definition lt := lt_list. - Hint Unfold lt. + Hint Unfold lt : core. Instance lt_strorder : StrictOrder lt. Proof. @@ -933,13 +933,13 @@ Module MakeListOrdering (O:OrderedType). left; MO.order. right; rewrite <- E12; auto. left; MO.order. right; rewrite E12; auto. Qed. - Hint Resolve eq_cons. + Hint Resolve eq_cons : core. Lemma cons_CompSpec : forall c x1 x2 l1 l2, O.eq x1 x2 -> CompSpec eq lt l1 l2 c -> CompSpec eq lt (x1::l1) (x2::l2) c. Proof. destruct c; simpl; inversion_clear 2; auto with relations. Qed. - Hint Resolve cons_CompSpec. + Hint Resolve cons_CompSpec : core. End MakeListOrdering. diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index 35fe4cee4e..7b64818b24 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -231,14 +231,14 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Notation In := (InA X.eq). Existing Instance X.eq_equiv. - Hint Extern 20 => solve [order]. + Hint Extern 20 => solve [order] : core. Definition IsOk s := Sort s. Class Ok (s:t) : Prop := ok : Sort s. - Hint Resolve ok. - Hint Unfold Ok. + Hint Resolve ok : core. + Hint Unfold Ok : core. Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }. @@ -276,7 +276,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. destruct H; constructor; tauto. Qed. - Hint Extern 1 (Ok _) => rewrite <- isok_iff. + Hint Extern 1 (Ok _) => rewrite <- isok_iff : core. Ltac inv_ok := match goal with | H:sort X.lt (_ :: _) |- _ => inversion_clear H; inv_ok @@ -326,7 +326,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. intuition. intros; elim_compare x a; inv; intuition. Qed. - Hint Resolve add_inf. + Hint Resolve add_inf : core. Global Instance add_ok s x : forall `(Ok s), Ok (add x s). Proof. @@ -353,7 +353,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. intros; elim_compare x a; inv; auto. apply Inf_lt with a; auto. Qed. - Hint Resolve remove_inf. + Hint Resolve remove_inf : core. Global Instance remove_ok s x : forall `(Ok s), Ok (remove x s). Proof. @@ -396,7 +396,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. induction2. Qed. - Hint Resolve union_inf. + Hint Resolve union_inf : core. Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s'). Proof. @@ -422,7 +422,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. apply Hrec'; auto. apply Inf_lt with x'; auto. Qed. - Hint Resolve inter_inf. + Hint Resolve inter_inf : core. Global Instance inter_ok s s' : forall `(Ok s, Ok s'), Ok (inter s s'). Proof. @@ -452,7 +452,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. apply Hrec'; auto. apply Inf_lt with x'; auto. Qed. - Hint Resolve diff_inf. + Hint Resolve diff_inf : core. Global Instance diff_ok s s' : forall `(Ok s, Ok s'), Ok (diff s s'). Proof. diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v index 3c7dea736b..29e57ff0a2 100644 --- a/theories/MSets/MSetProperties.v +++ b/theories/MSets/MSetProperties.v @@ -21,7 +21,7 @@ Require Import DecidableTypeEx OrdersLists MSetFacts MSetDecide. Set Implicit Arguments. Unset Strict Implicit. -Hint Unfold transpose. +Hint Unfold transpose : core. (** First, a functor for Weak Sets in functorial version. *) @@ -735,7 +735,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). Proof. intros; rewrite cardinal_Empty; auto. Qed. - Hint Resolve cardinal_inv_1. + Hint Resolve cardinal_inv_1 : core. Lemma cardinal_inv_2 : forall s n, cardinal s = S n -> { x : elt | In x s }. @@ -774,7 +774,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). exact Equal_cardinal. Qed. - Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal. + Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : core. (** ** Cardinal and set operators *) @@ -898,7 +898,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). auto with set. Qed. - Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2. + Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : core. End WPropertiesOn. @@ -922,7 +922,7 @@ Module OrdProperties (M:Sets). Import M.E. Import M. - Hint Resolve elements_spec2. + Hint Resolve elements_spec2 : core. Hint Immediate min_elt_spec1 min_elt_spec2 min_elt_spec3 max_elt_spec1 max_elt_spec2 max_elt_spec3 : set. @@ -961,7 +961,7 @@ Module OrdProperties (M:Sets). Proof. intros a b H; unfold leb. rewrite H; auto. Qed. - Hint Resolve gtb_compat leb_compat. + Hint Resolve gtb_compat leb_compat : core. Lemma elements_split : forall x s, elements s = elements_lt x s ++ elements_ge x s. diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index eab01a55b0..f9105fdf74 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -450,13 +450,13 @@ Include MSetGenTree.Props X Color. Local Notation Rd := (Node Red). Local Notation Bk := (Node Black). -Local Hint Immediate MX.eq_sym. -Local Hint Unfold In lt_tree gt_tree Ok. -Local Hint Constructors InT bst. -Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok. -Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node. -Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans. -Local Hint Resolve elements_spec2. +Local Hint Immediate MX.eq_sym : core. +Local Hint Unfold In lt_tree gt_tree Ok : core. +Local Hint Constructors InT bst : core. +Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok : core. +Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core. +Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core. +Local Hint Resolve elements_spec2 : core. (** ** Singleton set *) @@ -1136,7 +1136,7 @@ Record INV l1 l2 acc : Prop := { acc_sorted : sort X.lt acc; l1_lt_acc x y : InA X.eq x l1 -> InA X.eq y acc -> X.lt x y; l2_lt_acc x y : InA X.eq x l2 -> InA X.eq y acc -> X.lt x y}. -Local Hint Resolve l1_sorted l2_sorted acc_sorted. +Local Hint Resolve l1_sorted l2_sorted acc_sorted : core. Lemma INV_init s1 s2 `(Ok s1, Ok s2) : INV (rev_elements s1) (rev_elements s2) nil. @@ -1506,8 +1506,8 @@ Class Rbt (t:tree) := RBT : exists d, rbt d t. (** ** Basic tactics and results about red-black *) Scheme rbt_ind := Induction for rbt Sort Prop. -Local Hint Constructors rbt rrt arbt. -Local Hint Extern 0 (notred _) => (exact I). +Local Hint Constructors rbt rrt arbt : core. +Local Hint Extern 0 (notred _) => (exact I) : core. Ltac invrb := intros; invtree rrt; invtree rbt; try contradiction. Ltac desarb := match goal with H:arbt _ _ |- _ => destruct H end. Ltac nonzero n := destruct n as [|n]; [try split; invrb|]. @@ -1519,7 +1519,7 @@ Proof. destruct l, r; descolor; invrb; auto. Qed. -Local Hint Resolve rr_nrr_rb. +Local Hint Resolve rr_nrr_rb : core. Lemma arb_nrr_rb n t : arbt n t -> notredred t -> rbt n t. @@ -1533,7 +1533,7 @@ Proof. destruct 1; destruct t; descolor; invrb; auto. Qed. -Local Hint Resolve arb_nrr_rb arb_nr_rb. +Local Hint Resolve arb_nrr_rb arb_nr_rb : core. (** ** A Red-Black tree has indeed a logarithmic depth *) diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v index 8df1ff1cdb..19058a767e 100644 --- a/theories/MSets/MSetWeakList.v +++ b/theories/MSets/MSetWeakList.v @@ -123,15 +123,15 @@ Module MakeRaw (X:DecidableType) <: WRawSets X. Let eqr:= (@Equivalence_Reflexive _ _ X.eq_equiv). Let eqsym:= (@Equivalence_Symmetric _ _ X.eq_equiv). Let eqtrans:= (@Equivalence_Transitive _ _ X.eq_equiv). - Hint Resolve eqr eqtrans. - Hint Immediate eqsym. + Hint Resolve eqr eqtrans : core. + Hint Immediate eqsym : core. Definition IsOk := NoDup. Class Ok (s:t) : Prop := ok : NoDup s. - Hint Unfold Ok. - Hint Resolve ok. + Hint Unfold Ok : core. + Hint Resolve ok : core. Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }. diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 784e81758c..4bcd22543f 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -60,7 +60,7 @@ Section ZModulo. apply Z.lt_gt. unfold wB, base; auto with zarith. Qed. - Hint Resolve wB_pos. + Hint Resolve wB_pos : core. Lemma spec_to_Z_1 : forall x, 0 <= [|x|]. Proof. @@ -71,7 +71,7 @@ Section ZModulo. Proof. unfold to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto. Qed. - Hint Resolve spec_to_Z_1 spec_to_Z_2. + Hint Resolve spec_to_Z_1 spec_to_Z_2 : core. Lemma spec_to_Z : forall x, 0 <= [|x|] < wB. Proof. @@ -732,7 +732,7 @@ Section ZModulo. Proof. induction p; simpl; auto with zarith. Qed. - Hint Resolve Ptail_pos. + Hint Resolve Ptail_pos : core. Lemma Ptail_bounded : forall p d, Zpos p < 2^(Zpos d) -> Ptail p < Zpos d. Proof. diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 8e1be0d702..4539dea276 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -383,7 +383,7 @@ f_equiv. apply E, half_decrease. rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H. order'. Qed. -Hint Resolve log_good_step. +Hint Resolve log_good_step : core. Theorem log_init : forall n, n < 2 -> log n == 0. Proof. diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index c2316689fc..d86112abc0 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -26,7 +26,7 @@ Arguments id {A} x. Definition compose {A B C} (g : B -> C) (f : A -> B) := fun x : A => g (f x). -Hint Unfold compose. +Hint Unfold compose : core. Declare Scope program_scope. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 8479b9a2bb..f9d23e3cf6 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -110,7 +110,7 @@ Section Measure_well_founded. End Measure_well_founded. -Hint Resolve measure_wf. +Hint Resolve measure_wf : core. Section Fix_rects. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 81c318138e..f18fca99a0 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -66,7 +66,7 @@ Proof. rewrite hq, hq' in H'. subst q'. f_equal. apply eq_proofs_unicity. intros. repeat decide equality. Qed. -Hint Resolve Qc_is_canon. +Hint Resolve Qc_is_canon : core. Theorem Qc_decomp: forall q q': Qc, (q:Q) = q' -> q = q'. Proof. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index c832962590..b4c869b4dd 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -21,7 +21,7 @@ intros. now apply not_O_IZR. Qed. -Hint Resolve IZR_nz Rmult_integral_contrapositive. +Hint Resolve IZR_nz Rmult_integral_contrapositive : core. Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y. Proof. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 59a1049654..ec283b886e 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1087,7 +1087,7 @@ Proof. replace (r2 + r1 + - r2) with r1 by ring. exact H. Qed. -Hint Resolve Ropp_gt_lt_contravar. +Hint Resolve Ropp_gt_lt_contravar : core. Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2. Proof. @@ -1204,7 +1204,7 @@ Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r. Proof. intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real. Qed. -Hint Resolve Rmult_lt_compat_r. +Hint Resolve Rmult_lt_compat_r : core. Lemma Rmult_gt_compat_r : forall r r1 r2, r > 0 -> r1 > r2 -> r1 * r > r2 * r. Proof. eauto using Rmult_lt_compat_r with rorders. Qed. diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index 3977097e8c..61fe55770b 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -95,7 +95,7 @@ End Bounds. Hint Resolve Totally_ordered_definition Upper_Bound_definition Lower_Bound_definition Lub_definition Glb_definition Bottom_definition Definition_of_Complete Definition_of_Complete - Definition_of_Conditionally_complete. + Definition_of_Conditionally_complete : core. Section Specific_orders. Variable U : Type. diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v index bdeeb6a7c7..a0271a88a3 100644 --- a/theories/Sets/Infinite_sets.v +++ b/theories/Sets/Infinite_sets.v @@ -46,7 +46,7 @@ Section Approx. Defn_of_Approximant : Finite U X -> Included U X A -> Approximant A X. End Approx. -Hint Resolve Defn_of_Approximant. +Hint Resolve Defn_of_Approximant : core. Section Infinite_sets. Variable U : Type. diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index 88bcd6555c..50a7e401f8 100644 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v @@ -38,43 +38,43 @@ Variable U : Type. Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) := Definition_of_Power_set : forall X:Ensemble U, Included U X A -> In (Ensemble U) (Power_set A) X. -Hint Resolve Definition_of_Power_set. +Hint Resolve Definition_of_Power_set : core. Theorem Empty_set_minimal : forall X:Ensemble U, Included U (Empty_set U) X. intro X; red. intros x H'; elim H'. Qed. -Hint Resolve Empty_set_minimal. +Hint Resolve Empty_set_minimal : core. Theorem Power_set_Inhabited : forall X:Ensemble U, Inhabited (Ensemble U) (Power_set X). intro X. apply Inhabited_intro with (Empty_set U); auto with sets. Qed. -Hint Resolve Power_set_Inhabited. +Hint Resolve Power_set_Inhabited : core. Theorem Inclusion_is_an_order : Order (Ensemble U) (Included U). auto 6 with sets. Qed. -Hint Resolve Inclusion_is_an_order. +Hint Resolve Inclusion_is_an_order : core. Theorem Inclusion_is_transitive : Transitive (Ensemble U) (Included U). elim Inclusion_is_an_order; auto with sets. Qed. -Hint Resolve Inclusion_is_transitive. +Hint Resolve Inclusion_is_transitive : core. Definition Power_set_PO : Ensemble U -> PO (Ensemble U). intro A; try assumption. apply Definition_of_PO with (Power_set A) (Included U); auto with sets. Defined. -Hint Unfold Power_set_PO. +Hint Unfold Power_set_PO : core. Theorem Strict_Rel_is_Strict_Included : same_relation (Ensemble U) (Strict_Included U) (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))). auto with sets. Qed. -Hint Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included. +Hint Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included : core. Lemma Strict_inclusion_is_transitive_with_inclusion : forall x y z:Ensemble U, @@ -109,7 +109,7 @@ Theorem Empty_set_is_Bottom : forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U). intro A; apply Bottom_definition; simpl; auto with sets. Qed. -Hint Resolve Empty_set_is_Bottom. +Hint Resolve Empty_set_is_Bottom : core. Theorem Union_minimal : forall a b X:Ensemble U, @@ -117,7 +117,7 @@ Theorem Union_minimal : intros a b X H' H'0; red. intros x H'1; elim H'1; auto with sets. Qed. -Hint Resolve Union_minimal. +Hint Resolve Union_minimal : core. Theorem Intersection_maximal : forall a b X:Ensemble U, @@ -145,7 +145,7 @@ intros a b; red. intros x H'; elim H'; auto with sets. Qed. Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l - Intersection_decreases_r. + Intersection_decreases_r : core. Theorem Union_is_Lub : forall A a b:Ensemble U, diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index 296ec42add..d275487e15 100644 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v @@ -52,7 +52,7 @@ intros x y z h; elim h; intros H'3 H'4; clear h. intro h; elim h; intros H'5 H'6; clear h. split; apply H'1 with y; auto 10 with sets. Qed. -Hint Resolve Equiv_from_preorder. +Hint Resolve Equiv_from_preorder : core. Theorem Equiv_from_order : forall (U:Type) (R:Relation U), @@ -60,21 +60,21 @@ Theorem Equiv_from_order : Proof. intros U R H'; elim H'; auto 10 with sets. Qed. -Hint Resolve Equiv_from_order. +Hint Resolve Equiv_from_order : core. Theorem contains_is_preorder : forall U:Type, Preorder (Relation U) (contains U). Proof. auto 10 with sets. Qed. -Hint Resolve contains_is_preorder. +Hint Resolve contains_is_preorder : core. Theorem same_relation_is_equivalence : forall U:Type, Equivalence (Relation U) (same_relation U). Proof. unfold same_relation at 1; auto 10 with sets. Qed. -Hint Resolve same_relation_is_equivalence. +Hint Resolve same_relation_is_equivalence : core. Theorem cong_reflexive_same_relation : forall (U:Type) (R R':Relation U), diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index 0c1f670d0e..18ea019526 100644 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -38,7 +38,7 @@ Proof. intros U R x y H'; red. exists y; auto with sets. Qed. -Hint Resolve Rstar_imp_coherent. +Hint Resolve Rstar_imp_coherent : core. Theorem coherent_symmetric : forall (U:Type) (R:Relation U), Symmetric U (coherent U R). diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 7940bda1a7..0ff304ed6b 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -41,21 +41,21 @@ Definition Singleton (a:A) := end). Definition In (s:uniset) (a:A) : Prop := charac s a = true. -Hint Unfold In. +Hint Unfold In : core. (** uniset inclusion *) Definition incl (s1 s2:uniset) := forall a:A, leb (charac s1 a) (charac s2 a). -Hint Unfold incl. +Hint Unfold incl : core. (** uniset equality *) Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a. -Hint Unfold seq. +Hint Unfold seq : core. Lemma leb_refl : forall b:bool, leb b b. Proof. destruct b; simpl; auto. Qed. -Hint Resolve leb_refl. +Hint Resolve leb_refl : core. Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2. Proof. @@ -71,7 +71,7 @@ Lemma seq_refl : forall x:uniset, seq x x. Proof. destruct x; unfold seq; auto. Qed. -Hint Resolve seq_refl. +Hint Resolve seq_refl : core. Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z. Proof. @@ -94,21 +94,21 @@ Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x). Proof. unfold seq; unfold union; simpl; auto. Qed. -Hint Resolve union_empty_left. +Hint Resolve union_empty_left : core. Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset). Proof. unfold seq; unfold union; simpl. intros x a; rewrite (orb_b_false (charac x a)); auto. Qed. -Hint Resolve union_empty_right. +Hint Resolve union_empty_right : core. Lemma union_comm : forall x y:uniset, seq (union x y) (union y x). Proof. unfold seq; unfold charac; unfold union. destruct x; destruct y; auto with bool. Qed. -Hint Resolve union_comm. +Hint Resolve union_comm : core. Lemma union_ass : forall x y z:uniset, seq (union (union x y) z) (union x (union y z)). @@ -116,7 +116,7 @@ Proof. unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z; auto with bool. Qed. -Hint Resolve union_ass. +Hint Resolve union_ass : core. Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z). Proof. @@ -124,7 +124,7 @@ unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z. intros; elim H; auto. Qed. -Hint Resolve seq_left. +Hint Resolve seq_left : core. Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y). Proof. @@ -132,7 +132,7 @@ unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z. intros; elim H; auto. Qed. -Hint Resolve seq_right. +Hint Resolve seq_right : core. (** All the proofs that follow duplicate [Multiset_of_A] *) diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 2ef162be4e..6a22501afa 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -36,8 +36,8 @@ Section defs. Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z. Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y. - Hint Resolve leA_refl. - Hint Immediate eqA_dec leA_dec leA_antisym. + Hint Resolve leA_refl : core. + Hint Immediate eqA_dec leA_dec leA_antisym : core. Let emptyBag := EmptyBag A. Let singletonBag := SingletonBag _ eqA_dec. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 7b99b3626f..f5bc9eee4e 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -31,7 +31,7 @@ Inductive Permutation : list A -> list A -> Prop := | perm_trans l l' l'' : Permutation l l' -> Permutation l' l'' -> Permutation l l''. -Local Hint Constructors Permutation. +Local Hint Constructors Permutation : core. (** Some facts about [Permutation] *) @@ -71,13 +71,13 @@ Qed. End Permutation. -Hint Resolve Permutation_refl perm_nil perm_skip. +Hint Resolve Permutation_refl perm_nil perm_skip : core. (* These hints do not reduce the size of the problem to solve and they must be used with care to avoid combinatoric explosions *) -Local Hint Resolve perm_swap perm_trans. -Local Hint Resolve Permutation_sym Permutation_trans. +Local Hint Resolve perm_swap perm_trans : core. +Local Hint Resolve Permutation_sym Permutation_trans : core. (* This provides reflexivity, symmetry and transitivity and rewriting on morphims to come *) @@ -156,7 +156,7 @@ Qed. Lemma Permutation_cons_append : forall (l : list A) x, Permutation (x :: l) (l ++ x :: nil). Proof. induction l; intros; auto. simpl. rewrite <- IHl; auto. Qed. -Local Hint Resolve Permutation_cons_append. +Local Hint Resolve Permutation_cons_append : core. Theorem Permutation_app_comm : forall (l l' : list A), Permutation (l ++ l') (l' ++ l). @@ -166,7 +166,7 @@ Proof. rewrite app_comm_cons, Permutation_cons_append. now rewrite <- app_assoc. Qed. -Local Hint Resolve Permutation_app_comm. +Local Hint Resolve Permutation_app_comm : core. Theorem Permutation_cons_app : forall (l l1 l2:list A) a, Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2). @@ -175,7 +175,7 @@ Proof. rewrite app_comm_cons, Permutation_cons_append. now rewrite <- app_assoc. Qed. -Local Hint Resolve Permutation_cons_app. +Local Hint Resolve Permutation_cons_app : core. Lemma Permutation_Add a l l' : Add a l l' -> Permutation (a::l) l'. Proof. @@ -188,7 +188,7 @@ Theorem Permutation_middle : forall (l1 l2:list A) a, Proof. auto. Qed. -Local Hint Resolve Permutation_middle. +Local Hint Resolve Permutation_middle : core. Theorem Permutation_rev : forall (l : list A), Permutation l (rev l). Proof. diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 89e9c7f3e1..6782dd9ca3 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -137,8 +137,8 @@ Section defs. End defs. -Hint Constructors HdRel. -Hint Constructors Sorted. +Hint Constructors HdRel : core. +Hint Constructors Sorted : core. (* begin hide *) (* Compatibility with deprecated file Sorting.v *) diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index 24333ad815..f82ca5fa3c 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -38,8 +38,8 @@ Module KeyDecidableType(D:DecidableType). Definition eqke (p p':key*elt) := eq (fst p) (fst p') /\ (snd p) = (snd p'). - Hint Unfold eqk eqke. - Hint Extern 2 (eqke ?a ?b) => split. + Hint Unfold eqk eqke : core. + Hint Extern 2 (eqke ?a ?b) => split : core. (* eqke is stricter than eqk *) @@ -70,8 +70,8 @@ Module KeyDecidableType(D:DecidableType). unfold eqke; intuition; [ eauto | congruence ]. Qed. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. - Hint Immediate eqk_sym eqke_sym. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. + Hint Immediate eqk_sym eqke_sym : core. Global Instance eqk_equiv : Equivalence eqk. Proof. split; eauto. Qed. @@ -84,7 +84,7 @@ Module KeyDecidableType(D:DecidableType). Proof. unfold eqke; induction 1; intuition. Qed. - Hint Resolve InA_eqke_eqk. + Hint Resolve InA_eqke_eqk : core. Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. Proof. @@ -94,7 +94,7 @@ Module KeyDecidableType(D:DecidableType). Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). Definition In k m := exists e:elt, MapsTo k e m. - Hint Unfold MapsTo In. + Hint Unfold MapsTo In : core. (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) @@ -140,13 +140,13 @@ Module KeyDecidableType(D:DecidableType). End Elt. - Hint Unfold eqk eqke. - Hint Extern 2 (eqke ?a ?b) => split. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. - Hint Immediate eqk_sym eqke_sym. - Hint Resolve InA_eqke_eqk. - Hint Unfold MapsTo In. - Hint Resolve In_inv_2 In_inv_3. + Hint Unfold eqk eqke : core. + Hint Extern 2 (eqke ?a ?b) => split : core. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. + Hint Immediate eqk_sym eqke_sym : core. + Hint Resolve InA_eqke_eqk : core. + Hint Unfold MapsTo In : core. + Hint Resolve In_inv_2 In_inv_3 : core. End KeyDecidableType. diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index 5f60a979c6..4143dba547 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -53,8 +53,8 @@ Module Type IsEqOrig (Import E:Eq'). Axiom eq_refl : forall x : t, x==x. Axiom eq_sym : forall x y : t, x==y -> y==x. Axiom eq_trans : forall x y z : t, x==y -> y==z -> x==z. - Hint Immediate eq_sym. - Hint Resolve eq_refl eq_trans. + Hint Immediate eq_sym : core. + Hint Resolve eq_refl eq_trans : core. End IsEqOrig. (** * Types with decidable equality *) diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v index 7b6ee2eaca..c738b57f44 100644 --- a/theories/Structures/EqualitiesFacts.v +++ b/theories/Structures/EqualitiesFacts.v @@ -22,7 +22,7 @@ Module KeyDecidableType(D:DecidableType). Definition eqk {elt} : relation (key*elt) := D.eq @@1. Definition eqke {elt} : relation (key*elt) := D.eq * Logic.eq. - Hint Unfold eqk eqke. + Hint Unfold eqk eqke : core. (** eqk, eqke are equalities *) @@ -60,7 +60,7 @@ Module KeyDecidableType(D:DecidableType). Lemma eqk_1 {elt} k k' (e e':elt) : eqk (k,e) (k',e') -> D.eq k k'. Proof. trivial. Qed. - Hint Resolve eqke_1 eqke_2 eqk_1. + Hint Resolve eqke_1 eqke_2 eqk_1 : core. (* Additional facts *) @@ -69,7 +69,7 @@ Module KeyDecidableType(D:DecidableType). Proof. induction 1; firstorder. Qed. - Hint Resolve InA_eqke_eqk. + Hint Resolve InA_eqke_eqk : core. Lemma InA_eqk_eqke {elt} p (m:list (key*elt)) : InA eqk p m -> exists q, eqk p q /\ InA eqke q m. @@ -86,7 +86,7 @@ Module KeyDecidableType(D:DecidableType). Definition MapsTo {elt} (k:key)(e:elt):= InA eqke (k,e). Definition In {elt} k m := exists e:elt, MapsTo k e m. - Hint Unfold MapsTo In. + Hint Unfold MapsTo In : core. (* Alternative formulations for [In k l] *) @@ -167,9 +167,9 @@ Module KeyDecidableType(D:DecidableType). eauto with *. Qed. - Hint Extern 2 (eqke ?a ?b) => split. - Hint Resolve InA_eqke_eqk. - Hint Resolve In_inv_2 In_inv_3. + Hint Extern 2 (eqke ?a ?b) => split : core. + Hint Resolve InA_eqke_eqk : core. + Hint Resolve In_inv_2 In_inv_3 : core. End KeyDecidableType. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index f6fc247d5a..d000b75bf4 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -42,8 +42,8 @@ Module Type MiniOrderedType. Parameter compare : forall x y : t, Compare lt eq x y. - Hint Immediate eq_sym. - Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. + Hint Immediate eq_sym : core. + Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : core. End MiniOrderedType. @@ -143,9 +143,9 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma eq_not_gt x y : eq x y -> ~ lt y x. Proof. order. Qed. Lemma lt_not_gt x y : lt x y -> ~ lt y x. Proof. order. Qed. - Hint Resolve gt_not_eq eq_not_lt. - Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq. - Hint Resolve eq_not_gt lt_antirefl lt_not_gt. + Hint Resolve gt_not_eq eq_not_lt : core. + Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq : core. + Hint Resolve eq_not_gt lt_antirefl lt_not_gt : core. Lemma elim_compare_eq : forall x y : t, @@ -247,8 +247,8 @@ Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat). Qed. End ForNotations. -Hint Resolve ListIn_In Sort_NoDup Inf_lt. -Hint Immediate In_eq Inf_lt. +Hint Resolve ListIn_In Sort_NoDup Inf_lt : core. +Hint Immediate In_eq Inf_lt : core. End OrderedTypeFacts. @@ -266,8 +266,8 @@ Module KeyOrderedType(O:OrderedType). eq (fst p) (fst p') /\ (snd p) = (snd p'). Definition ltk (p p':key*elt) := lt (fst p) (fst p'). - Hint Unfold eqk eqke ltk. - Hint Extern 2 (eqke ?a ?b) => split. + Hint Unfold eqk eqke ltk : core. + Hint Extern 2 (eqke ?a ?b) => split : core. (* eqke is stricter than eqk *) @@ -283,7 +283,7 @@ Module KeyOrderedType(O:OrderedType). Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x. Proof. auto. Qed. - Hint Immediate ltk_right_r ltk_right_l. + Hint Immediate ltk_right_r ltk_right_l : core. (* eqk, eqke are equalities, ltk is a strict order *) @@ -319,9 +319,9 @@ Module KeyOrderedType(O:OrderedType). exact (lt_not_eq H H1). Qed. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. - Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke. - Hint Immediate eqk_sym eqke_sym. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. + Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : core. + Hint Immediate eqk_sym eqke_sym : core. Global Instance eqk_equiv : Equivalence eqk. Proof. constructor; eauto. Qed. @@ -359,22 +359,22 @@ Module KeyOrderedType(O:OrderedType). intros (k,e) (k',e') (k'',e''). unfold ltk, eqk; simpl; eauto. Qed. - Hint Resolve eqk_not_ltk. - Hint Immediate ltk_eqk eqk_ltk. + Hint Resolve eqk_not_ltk : core. + Hint Immediate ltk_eqk eqk_ltk : core. Lemma InA_eqke_eqk : forall x m, InA eqke x m -> InA eqk x m. Proof. unfold eqke; induction 1; intuition. Qed. - Hint Resolve InA_eqke_eqk. + Hint Resolve InA_eqke_eqk : core. Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). Definition In k m := exists e:elt, MapsTo k e m. Notation Sort := (sort ltk). Notation Inf := (lelistA ltk). - Hint Unfold MapsTo In. + Hint Unfold MapsTo In : core. (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) @@ -405,8 +405,8 @@ Module KeyOrderedType(O:OrderedType). Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. Proof. exact (InfA_ltA ltk_strorder). Qed. - Hint Immediate Inf_eq. - Hint Resolve Inf_lt. + Hint Immediate Inf_eq : core. + Hint Resolve Inf_lt : core. Lemma Sort_Inf_In : forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p. @@ -469,19 +469,19 @@ Module KeyOrderedType(O:OrderedType). End Elt. - Hint Unfold eqk eqke ltk. - Hint Extern 2 (eqke ?a ?b) => split. - Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl. - Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke. - Hint Immediate eqk_sym eqke_sym. - Hint Resolve eqk_not_ltk. - Hint Immediate ltk_eqk eqk_ltk. - Hint Resolve InA_eqke_eqk. - Hint Unfold MapsTo In. - Hint Immediate Inf_eq. - Hint Resolve Inf_lt. - Hint Resolve Sort_Inf_NotIn. - Hint Resolve In_inv_2 In_inv_3. + Hint Unfold eqk eqke ltk : core. + Hint Extern 2 (eqke ?a ?b) => split : core. + Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. + Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : core. + Hint Immediate eqk_sym eqke_sym : core. + Hint Resolve eqk_not_ltk : core. + Hint Immediate ltk_eqk eqk_ltk : core. + Hint Resolve InA_eqke_eqk : core. + Hint Unfold MapsTo In : core. + Hint Immediate Inf_eq : core. + Hint Resolve Inf_lt : core. + Hint Resolve Sort_Inf_NotIn : core. + Hint Resolve In_inv_2 In_inv_3 : core. End KeyOrderedType. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index 42756ad339..310a22a0a4 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -181,7 +181,7 @@ Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder we coerce [bool] into [Prop]. *) Local Coercion is_true : bool >-> Sortclass. -Hint Unfold is_true. +Hint Unfold is_true : core. Module Type HasLeb (Import T:Typ). Parameter Inline leb : t -> t -> bool. diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v index abdb9eff05..fef9b14a9e 100644 --- a/theories/Structures/OrdersLists.v +++ b/theories/Structures/OrdersLists.v @@ -50,8 +50,8 @@ Proof. exact (InfA_alt O.eq_equiv O.lt_strorder O.lt_compat). Qed. Lemma Sort_NoDup : forall l, Sort l -> NoDup l. Proof. exact (SortA_NoDupA O.eq_equiv O.lt_strorder O.lt_compat) . Qed. -Hint Resolve ListIn_In Sort_NoDup Inf_lt. -Hint Immediate In_eq Inf_lt. +Hint Resolve ListIn_In Sort_NoDup Inf_lt : core. +Hint Immediate In_eq Inf_lt : core. End OrderedTypeLists. @@ -66,7 +66,7 @@ Module KeyOrderedType(O:OrderedType). Definition ltk {elt} : relation (key*elt) := O.lt @@1. - Hint Unfold ltk. + Hint Unfold ltk : core. (* ltk is a strict order *) @@ -109,8 +109,8 @@ Module KeyOrderedType(O:OrderedType). Lemma Inf_lt l x x' : ltk x x' -> Inf x' l -> Inf x l. Proof. apply InfA_ltA; auto with *. Qed. - Hint Immediate Inf_eq. - Hint Resolve Inf_lt. + Hint Immediate Inf_eq : core. + Hint Resolve Inf_lt : core. Lemma Sort_Inf_In l p q : Sort l -> Inf q l -> InA eqk p l -> ltk q p. Proof. apply SortA_InfA_InA; auto with *. Qed. @@ -148,10 +148,10 @@ Module KeyOrderedType(O:OrderedType). End Elt. - Hint Resolve ltk_not_eqk ltk_not_eqke. - Hint Immediate Inf_eq. - Hint Resolve Inf_lt. - Hint Resolve Sort_Inf_NotIn. + Hint Resolve ltk_not_eqk ltk_not_eqke : core. + Hint Immediate Inf_eq : core. + Hint Resolve Inf_lt : core. + Hint Resolve Sort_Inf_NotIn : core. End KeyOrderedType. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 4a2bddf35c..7f96aa6b87 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -269,28 +269,28 @@ Section SCANNING. Inductive Forall {A} (P: A -> Prop): forall {n} (v: t A n), Prop := |Forall_nil: Forall P [] |Forall_cons {n} x (v: t A n): P x -> Forall P v -> Forall P (x::v). -Hint Constructors Forall. +Hint Constructors Forall : core. Inductive Exists {A} (P:A->Prop): forall {n}, t A n -> Prop := |Exists_cons_hd {m} x (v: t A m): P x -> Exists P (x::v) |Exists_cons_tl {m} x (v: t A m): Exists P v -> Exists P (x::v). -Hint Constructors Exists. +Hint Constructors Exists : core. Inductive In {A} (a:A): forall {n}, t A n -> Prop := |In_cons_hd {m} (v: t A m): In a (a::v) |In_cons_tl {m} x (v: t A m): In a v -> In a (x::v). -Hint Constructors In. +Hint Constructors In : core. Inductive Forall2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop := |Forall2_nil: Forall2 P [] [] |Forall2_cons {m} x1 x2 (v1:t A m) v2: P x1 x2 -> Forall2 P v1 v2 -> Forall2 P (x1::v1) (x2::v2). -Hint Constructors Forall2. +Hint Constructors Forall2 : core. Inductive Exists2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop := |Exists2_cons_hd {m} x1 x2 (v1: t A m) (v2: t B m): P x1 x2 -> Exists2 P (x1::v1) (x2::v2) |Exists2_cons_tl {m} x1 x2 (v1:t A m) v2: Exists2 P v1 v2 -> Exists2 P (x1::v1) (x2::v2). -Hint Constructors Exists2. +Hint Constructors Exists2 : core. End SCANNING. diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index ff233ef9c6..18c4bedd9a 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -22,7 +22,7 @@ Section WfInclusion. apply Acc_intro; auto with sets. Qed. - Hint Resolve Acc_incl. + Hint Resolve Acc_incl : core. Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1. Proof. diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index 59068623ae..0d56d88869 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -31,7 +31,7 @@ Section Wf_Transitive_Closure. apply Acc_inv with y; auto with sets. Defined. - Hint Resolve Acc_clos_trans. + Hint Resolve Acc_clos_trans : core. Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y. Proof. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 74614e114a..c278cada61 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -73,7 +73,7 @@ Proof. intros; unfold Remainder, Remainder_alt; omega with *. Qed. -Hint Unfold Remainder. +Hint Unfold Remainder : core. (** Now comes the fully general result about Euclidean division. *) diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index 24412e9431..b8c7319939 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -47,7 +47,7 @@ Section Log_pos. (* Log of positive integers *) | xI n => Z.succ (Z.succ (log_inf n)) (* 2n+1 *) end. - Hint Unfold log_inf log_sup. + Hint Unfold log_inf log_sup : core. Lemma Psize_log_inf : forall p, Zpos (Pos.size p) = Z.succ (log_inf p). Proof. diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index e4d9e9ac25..66469ff0b9 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -107,7 +107,7 @@ let load_init_vernaculars cur_feeder opts ~state = (* Startup LoadPath and Modules *) (******************************************************************************) (* prelude_data == From Coq Require Export Prelude. *) -let prelude_data = "Prelude", Some "Coq", Some true +let prelude_data = "Prelude", Some "Coq", Some false let require_libs opts = if opts.load_init then prelude_data :: opts.vo_requires else opts.vo_requires diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 88638b295b..bc0b0310b3 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -9,7 +9,14 @@ (************************************************************************) open CErrors -open Vernacexpr + +(** The type of parsing attribute data *) +type vernac_flags = vernac_flag list +and vernac_flag = string * vernac_flag_value +and vernac_flag_value = + | VernacFlagEmpty + | VernacFlagLeaf of string + | VernacFlagList of vernac_flags let unsupported_attributes = function | [] -> () diff --git a/vernac/attributes.mli b/vernac/attributes.mli index c81082d5ad..c2dde4cbcc 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -8,7 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Vernacexpr +(** The type of parsing attribute data *) +type vernac_flags = vernac_flag list +and vernac_flag = string * vernac_flag_value +and vernac_flag_value = + | VernacFlagEmpty + | VernacFlagLeaf of string + | VernacFlagList of vernac_flags type +'a attribute (** The type of attributes. When parsing attributes if an ['a @@ -80,7 +86,7 @@ val parse_with_extra : 'a attribute -> vernac_flags -> vernac_flags * 'a (** * Defining attributes. *) -type 'a key_parser = 'a option -> Vernacexpr.vernac_flag_value -> 'a +type 'a key_parser = 'a option -> vernac_flag_value -> 'a (** A parser for some key in an attribute. It is given a nonempty ['a option] when the attribute is multiply set for some command. diff --git a/vernac/classes.ml b/vernac/classes.ml index b0dba2485a..95e46b252b 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -188,8 +188,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id ] in ignore (Pfedit.by init_refine) - else if Flags.is_auto_intros () then - ignore (Pfedit.by (Tactics.auto_intros_tac ids)); + else ignore (Pfedit.by (Tactics.auto_intros_tac ids)); (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) () let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = diff --git a/vernac/egramml.mli b/vernac/egramml.mli index a90ef97e7d..3689f60383 100644 --- a/vernac/egramml.mli +++ b/vernac/egramml.mli @@ -21,10 +21,10 @@ type 's grammar_prod_item = ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item val extend_vernac_command_grammar : - Vernacexpr.extend_name -> vernac_expr Pcoq.Entry.t option -> + extend_name -> vernac_expr Pcoq.Entry.t option -> vernac_expr grammar_prod_item list -> unit -val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list +val get_extend_vernac_rule : extend_name -> vernac_expr grammar_prod_item list val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 960e74827a..3cdf81ced0 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -30,6 +30,7 @@ open Pcoq.Prim open Pcoq.Constr open Pcoq.Module open Pvernac.Vernac_ +open Attributes let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] let _ = List.iter CLexer.add_keyword vernac_kw diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ba31f73030..6c7117b513 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -884,8 +884,6 @@ let explain_not_match_error = function let status b = if b then str"polymorphic" else str"monomorphic" in str "a " ++ status b ++ str" declaration was expected, but a " ++ status (not b) ++ str" declaration was found" - | IncompatibleInstances -> - str"polymorphic universe instances do not match" | IncompatibleUniverses incon -> str"the universe constraints are inconsistent: " ++ Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon @@ -894,11 +892,22 @@ let explain_not_match_error = function quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t1) ++ spc () ++ str "compared to " ++ spc () ++ quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2) - | IncompatibleConstraints cst -> - str " the expected (polymorphic) constraints do not imply " ++ - let cst = Univ.UContext.constraints (Univ.AUContext.repr cst) in - (** FIXME: provide a proper naming for the bound variables *) - quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst) + | IncompatibleConstraints { got; expect } -> + let open Univ in + let pr_auctx auctx = + let sigma = Evd.from_ctx + (UState.of_binders + (UnivNames.universe_binders_with_opt_names auctx None)) + in + let uctx = AUContext.repr auctx in + Printer.pr_universe_instance_constraints sigma + (UContext.instance uctx) + (UContext.constraints uctx) + in + str "incompatible polymorphic binders: got" ++ spc () ++ h 0 (pr_auctx got) ++ spc() ++ + str "but expected" ++ spc() ++ h 0 (pr_auctx expect) ++ + (if not (Int.equal (AUContext.size got) (AUContext.size expect)) then mt() else + fnl() ++ str "(incompatible constraints)") let explain_signature_mismatch l spec why = str "Signature components for label " ++ Label.print l ++ diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index d537436c6b..4e847a5590 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -306,17 +306,18 @@ let universe_proof_terminator compute_guard hook = | Admitted (id,k,pe,ctx) -> admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) (); Feedback.feedback Feedback.AddedAxiom - | Proved (opaque,idopt,proof) -> - let is_opaque, export_seff = match opaque with - | Transparent -> false, true - | Opaque -> true, false - in - let (id,(const,univs,persistence)) = Pfedit.cook_this_proof proof in - let const = {const with const_entry_opaque = is_opaque} in - let id = match idopt with - | None -> id - | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in - save ~export_seff id const univs compute_guard persistence (hook (Some univs)) + | Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) -> + let is_opaque, export_seff = match opaque with + | Transparent -> false, true + | Opaque -> true, false + in + let const = {const with const_entry_opaque = is_opaque} in + let id = match idopt with + | None -> id + | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in + save ~export_seff id const universes compute_guard persistence (hook (Some universes)) + | Proved (opaque,idopt, _ ) -> + CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term") end let standard_proof_terminator compute_guard hook = @@ -372,22 +373,17 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook = let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in let init_tac,guard = match recguard with | Some (finite,guard,init_tac) -> - let rec_tac = rec_tac_initializer finite guard thms snl in - Some (match init_tac with - | None -> - if Flags.is_auto_intros () then - Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms) - else - rec_tac + let rec_tac = rec_tac_initializer finite guard thms snl in + Some (match init_tac with + | None -> + Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms) | Some tacl -> - Tacticals.New.tclTHENS rec_tac - (if Flags.is_auto_intros () then - List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms - else - tacl)),guard + Tacticals.New.tclTHENS rec_tac + List.(map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms) + ),guard | None -> - let () = match thms with [_] -> () | _ -> assert false in - (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in + let () = match thms with [_] -> () | _ -> assert false in + Some (intro_tac (List.hd thms)), [] in match thms with | [] -> anomaly (Pp.str "No proof to start.") | (id,(t,(_,imps)))::other_thms -> diff --git a/vernac/obligations.ml b/vernac/obligations.ml index c2805674e4..746db61cc3 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -844,8 +844,7 @@ let obligation_terminator name num guard hook auto pf = let term = Lemmas.universe_proof_terminator guard hook in match pf with | Admitted _ -> apply_terminator term pf - | Proved (opq, id, proof) -> - let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in + | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin let env = Global.env () in let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in let ty = entry.Entries.const_entry_type in @@ -904,6 +903,9 @@ let obligation_terminator name num guard hook auto pf = with e when CErrors.noncritical e -> let e = CErrors.push e in pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) + end + | Proved (_, _, _ ) -> + CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term") let obligation_hook prg obl num auto ctx' _ gr = let obls, rem = prg.prg_obligations in diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f65fae60ee..2ddd210365 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1214,6 +1214,7 @@ open Pputils let rec pr_vernac_flag (k, v) = let k = keyword k in + let open Attributes in match v with | VernacFlagEmpty -> k | VernacFlagLeaf v -> k ++ str " = " ++ qs v diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index b2fa8ec99f..4761e4bbc2 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -42,7 +42,7 @@ module Vernac_ = let command_entry_ref = ref noedit_mode let command_entry = Gram.Entry.of_parser "command_entry" - (fun strm -> Gram.Entry.parse_token !command_entry_ref strm) + (fun strm -> Gram.Entry.parse_token_stream !command_entry_ref strm) end diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7765f5b417..df4193f397 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1098,13 +1098,28 @@ let vernac_restore_state file = let vernac_create_hintdb ~module_local id b = Hints.create_hint_db module_local id TransparentState.full b -let vernac_remove_hints ~module_local dbs ids = - Hints.remove_hints module_local dbs (List.map Smartlocate.global_with_alias ids) +let warn_implicit_core_hint_db = + CWarnings.create ~name:"implicit-core-hint-db" ~category:"deprecated" + (fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. " + ++ strbrk"Please specify a hint database.") + +let vernac_remove_hints ~module_local dbnames ids = + let dbnames = + if List.is_empty dbnames then + (warn_implicit_core_hint_db (); ["core"]) + else dbnames + in + Hints.remove_hints module_local dbnames (List.map Smartlocate.global_with_alias ids) -let vernac_hints ~atts lb h = +let vernac_hints ~atts dbnames h = + let dbnames = + if List.is_empty dbnames then + (warn_implicit_core_hint_db (); ["core"]) + else dbnames + in let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in let local = enforce_module_locality local in - Hints.add_hints ~local lb (Hints.interp_hints poly h) + Hints.add_hints ~local dbnames (Hints.interp_hints poly h) let vernac_syntactic_definition ~module_local lid x y = Dumpglob.dump_definition lid false "syndef"; @@ -1453,14 +1468,6 @@ let _ = let _ = declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "automatic introduction of variables"; - optkey = ["Automatic";"Introduction"]; - optread = Flags.is_auto_intros; - optwrite = Flags.make_auto_intros } - -let _ = - declare_bool_option { optdepr = false; optname = "coercion printing"; optkey = ["Printing";"Coercions"]; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 180d763946..122005e011 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -219,13 +219,6 @@ type section_subset_expr = {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 *) @@ -253,6 +246,14 @@ type vernac_argument_status = { implicit_status : vernac_implicit_status; } +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 + type nonrec vernac_expr = | VernacLoad of verbose_flag * string @@ -395,71 +396,11 @@ type nonrec vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list -type vernac_flags = vernac_flag list -and vernac_flag = string * vernac_flag_value -and vernac_flag_value = - | VernacFlagEmpty - | VernacFlagLeaf of string - | VernacFlagList of vernac_flags - type vernac_control = - | VernacExpr of vernac_flags * vernac_expr + | VernacExpr of Attributes.vernac_flags * 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 diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 5fba586298..3a321ecdb4 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -12,7 +12,43 @@ open Util open Pp open CErrors -type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t +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 { + parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; + proof_block_detection : proof_block_name option + } + (* 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 * Names.Id.t list +and vernac_sideff_type = Names.Id.t list +and opacity_guarantee = + | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) + | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) +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 + +type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t type plugin_args = Genarg.raw_generic_argument list @@ -68,10 +104,23 @@ let call opn converted_args ~atts ~st = (** VERNAC EXTEND registering *) -type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification +type classifier = Genarg.raw_generic_argument list -> vernac_classification + +(** Classifiers *) +let classifiers : classifier array String.Map.t ref = ref String.Map.empty + +let get_vernac_classifier (name, i) args = + (String.Map.find name !classifiers).(i) args + +let declare_vernac_classifier name f = + classifiers := String.Map.add name f !classifiers + +let classify_as_query = VtQuery, VtLater +let classify_as_sideeff = VtSideff [], VtLater +let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater type (_, _) ty_sig = -| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig +| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig @@ -124,7 +173,7 @@ let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s | TUentry a -> Aentry (Pcoq.genarg_grammar (Genarg.ExtraArg a)) | TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (Genarg.ExtraArg a), string_of_int i) -let rec untype_grammar : type r s. (r, s) ty_sig -> Vernacexpr.vernac_expr Egramml.grammar_prod_item list = function +let rec untype_grammar : type r s. (r, s) ty_sig -> 'a Egramml.grammar_prod_item list = function | TyNil -> [] | TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty | TyNonTerminal (tu, ty) -> @@ -132,16 +181,6 @@ let rec untype_grammar : type r s. (r, s) ty_sig -> Vernacexpr.vernac_expr Egram let symb = untype_user_symbol tu in Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty -let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol - -let classifiers : classifier array String.Map.t ref = ref String.Map.empty - -let get_vernac_classifier (name, i) args = - (String.Map.find name !classifiers).(i) args - -let declare_vernac_classifier name f = - classifiers := String.Map.add name f !classifiers - let vernac_extend ~command ?classifier ?entry ext = let get_classifier (TyML (_, ty, _, cl)) = match cl with | Some cl -> untype_classifier ty cl diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index bb94f3a6a9..7feaccd9a3 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -8,20 +8,75 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(** Vernacular Extension data *) + +(* 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 { + parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; + proof_block_detection : proof_block_name option + } + (* 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 * Names.Id.t list +and vernac_sideff_type = Names.Id.t list +and opacity_guarantee = + | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) + | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) +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 + (** Interpretation of extended vernac phrases. *) -type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t +type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t type plugin_args = Genarg.raw_generic_argument list -val call : Vernacexpr.extend_name -> plugin_args -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t +val call : Vernacexpr.extend_name -> plugin_args -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t (** {5 VERNAC EXTEND} *) -type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification +type classifier = Genarg.raw_generic_argument list -> vernac_classification type (_, _) ty_sig = -| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig +| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> @@ -32,7 +87,7 @@ type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> (** Wrapper to dynamically extend vernacular commands. *) val vernac_extend : command:string -> - ?classifier:(string -> Vernacexpr.vernac_classification) -> + ?classifier:(string -> vernac_classification) -> ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t -> ty_ml list -> unit @@ -55,6 +110,9 @@ val vernac_argument_extend : name:string -> 'a vernac_argument -> ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t (** {5 STM classifiers} *) +val get_vernac_classifier : Vernacexpr.extend_name -> classifier -val get_vernac_classifier : - Vernacexpr.extend_name -> classifier +(** Standard constant classifiers *) +val classify_as_query : vernac_classification +val classify_as_sideeff : vernac_classification +val classify_as_proofstep : vernac_classification |