diff options
Diffstat (limited to 'plugins')
26 files changed, 193 insertions, 224 deletions
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index c41687e721..b9274cf6b8 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -20,6 +20,7 @@ open Tacticals.New open Tacinterp open Stdarg open Tacarg +open Attributes open Pcoq.Prim } @@ -73,10 +74,9 @@ let (set_default_solver, default_solver, print_default_solver) = } VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF -| [ "Set" "Firstorder" "Solver" tactic(t) ] -> { - let open Vernacinterp in +| #[ locality; ] [ "Set" "Firstorder" "Solver" tactic(t) ] -> { set_default_solver - (Locality.make_section_locality atts.locality) + (Locality.make_section_locality locality) (Tacintern.glob_tactic t) } END diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ad1114b733..651895aa08 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -229,10 +229,6 @@ let isAppConstruct ?(env=Global.env ()) sigma t = true with Not_found -> false -let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) - Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env @@ Evd.from_env Environ.empty_env - - exception NoChange let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = @@ -420,7 +416,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = let rec scan_type context type_of_hyp : tactic = if isLetIn sigma type_of_hyp then let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in - let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in + let reduced_type_of_hyp = Reductionops.nf_betaiotazeta env sigma real_type_of_hyp in (* length of context didn't change ? *) let new_context,new_typ_of_hyp = decompose_prod_n_assum sigma (List.length context) reduced_type_of_hyp @@ -800,7 +796,7 @@ let build_proof g | LetIn _ -> let new_infos = - { dyn_infos with info = nf_betaiotazeta dyn_infos.info } + { dyn_infos with info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info } in tclTHENLIST @@ -834,7 +830,7 @@ let build_proof | LetIn _ -> let new_infos = { dyn_infos with - info = nf_betaiotazeta dyn_infos.info + info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info } in @@ -977,7 +973,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (* observe (str "body " ++ pr_lconstr bodies.(num)); *) let f_body_with_params_and_other_fun = substl fnames_with_params bodies.(num) in (* observe (str "f_body_with_params_and_other_fun " ++ pr_lconstr f_body_with_params_and_other_fun); *) - let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in + let eq_rhs = Reductionops.nf_betaiotazeta (Global.env ()) evd (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) let (type_ctxt,type_of_f),evd = let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f @@ -1008,7 +1004,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num Ensures by: obvious i*) (mk_equation_id f_id) - (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem)) + (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) evd lemma_type (Lemmas.mk_hook (fun _ _ -> ())); diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index d57b931785..d1e7d8a5a8 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -307,7 +307,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin begin Lemmas.start_proof new_princ_name - (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) + (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) !evd (EConstr.of_constr new_principle_type) hook @@ -359,10 +359,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let univs = - let poly = Flags.is_universe_polymorphism () in - Evd.const_univ_entry ~poly evd' - in + let univs = Evd.const_univ_entry ~poly:false evd' in let ce = Declare.definition_entry ~univs value in ignore( Declare.declare_constant diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 7c80b776a4..98aaa081c3 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1494,7 +1494,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters)) + (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds false false false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 9a6169d42a..35acbea488 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -414,7 +414,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ComDefinition.do_definition ~program_mode:false fname - (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl + (Decl_kinds.Global,false,Decl_kinds.Definition) pl bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); let evd,rev_pconstants = List.fold_left @@ -431,7 +431,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + ComFixpoint.do_fixpoint Global false fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index b0842c3721..d1a227d517 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -63,12 +63,6 @@ let observe_tac s tac g = then do_observe_tac (str s) tac g else tac g -(* [nf_zeta] $\zeta$-normalization of a term *) -let nf_zeta = - Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) - Environ.empty_env - (Evd.from_env Environ.empty_env) - let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl (* (\* [id_to_constr id] finds the term associated to [id] in the global environment *\) *) @@ -219,7 +213,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i let mib,_ = Global.lookup_inductive graph_ind in (* and the principle to use in this lemma in $\zeta$ normal form *) let f_principle,princ_type = schemes.(i) in - let princ_type = nf_zeta princ_type in + let princ_type = Reductionops.nf_zeta (Global.env ()) evd princ_type in let princ_infos = Tactics.compute_elim_sig evd princ_type in (* The number of args of the function is then easily computable *) let nb_fun_args = nb_prod (project g) (pf_concl g) - 2 in @@ -397,7 +391,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i List.rev (fst (List.fold_left2 (fun (bindings,avoid) decl p -> let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in - (nf_zeta p)::bindings,id::avoid) + (Reductionops.nf_zeta (pf_env g) (project g) p)::bindings,id::avoid) ([],avoid) princ_infos.predicates (lemmas))) @@ -630,12 +624,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti *) let lemmas = Array.map - (fun (_,(ctxt,concl)) -> nf_zeta (EConstr.it_mkLambda_or_LetIn concl ctxt)) + (fun (_,(ctxt,concl)) -> Reductionops.nf_zeta (pf_env g) (project g) (EConstr.it_mkLambda_or_LetIn concl ctxt)) lemmas_types_infos in (* We get the constant and the principle corresponding to this lemma *) let f = funcs.(i) in - let graph_principle = nf_zeta (EConstr.of_constr schemes.(i)) in + let graph_principle = Reductionops.nf_zeta (pf_env g) (project g) (EConstr.of_constr schemes.(i)) in let princ_type = pf_unsafe_type_of g graph_principle in let princ_infos = Tactics.compute_elim_sig (project g) princ_type in (* Then we get the number of argument of the function @@ -771,7 +765,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in evd := sigma; - let type_of_lemma = nf_zeta type_of_lemma in + let type_of_lemma = Reductionops.nf_zeta (Global.env ()) !evd type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma); type_of_lemma,type_info ) @@ -810,7 +804,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let (typ,_) = lemmas_types_infos.(i) in Lemmas.start_proof lem_id - (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem))) + (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem))) !evd typ (Lemmas.mk_hook (fun _ _ -> ())); @@ -838,7 +832,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in - let type_of_lemma = nf_zeta type_of_lemma in + let type_of_lemma = Reductionops.nf_zeta env !evd type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma); type_of_lemma,type_info ) @@ -872,7 +866,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list i*) let lem_id = mk_complete_id f_id in Lemmas.start_proof lem_id - (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma + (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma (fst lemmas_types_infos.(i)) (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index f9df3aed45..63a3e0582d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -103,21 +103,6 @@ let const_of_ref = function ConstRef kn -> kn | _ -> anomaly (Pp.str "ConstRef expected.") - -let nf_zeta env = - Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) - env (Evd.from_env env) - - -let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) - Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env - (Evd.from_env Environ.empty_env) - - - - - - (* Generic values *) let pf_get_new_ids idl g = let ids = pf_ids_of_hyps g in @@ -747,7 +732,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = with | UserError(Some "Refiner.thensn_tac3",_) | UserError(Some "Refiner.tclFAIL_s",_) -> - (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} ) + (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = Reductionops.nf_betaiotazeta (pf_env g) sigma new_info.info} ) )) g @@ -1537,13 +1522,13 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in let evd = Evd.minimize_universes evd in - let equation_lemma_type = nf_betaiotazeta (Evarutil.nf_evar evd ty) in + let equation_lemma_type = Reductionops.nf_betaiotazeta env evd (Evarutil.nf_evar evd ty) in let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *) let res_vars,eq' = decompose_prod equation_lemma_type in let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in - let eq' = nf_zeta env_eq' (EConstr.of_constr eq') in + let eq' = Reductionops.nf_zeta env_eq' evd (EConstr.of_constr eq') in let eq' = EConstr.Unsafe.to_constr eq' in let res = (* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *) diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index b660865e8b..85fb0c73c9 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -30,7 +30,7 @@ open Namegen open Tactypes open Tactics open Proofview.Notations -open Vernacinterp +open Attributes let wit_hyp = wit_var @@ -321,15 +321,15 @@ let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater } VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY { classify_hint } -| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> - { add_rewrite_hint ~poly:atts.polymorphic bl o None l } -| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) +| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> + { add_rewrite_hint ~poly:polymorphic bl o None l } +| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ":" preident_list(bl) ] -> - { add_rewrite_hint ~poly:atts.polymorphic bl o (Some t) l } -| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> - { add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l } -| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> - { add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l } + { add_rewrite_hint ~poly:polymorphic bl o (Some t) l } +| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> + { add_rewrite_hint ~poly:polymorphic ["core"] o None l } +| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> + { add_rewrite_hint ~poly:polymorphic ["core"] o (Some t) l } END (**********************************************************************) @@ -411,45 +411,39 @@ let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater END*) VERNAC COMMAND EXTEND DeriveInversionClear -| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] +| #[ polymorphic; ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] => { seff na } -> { - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac } + add_inversion_lemma_exn ~poly:polymorphic na c s false inv_clear_tac } -| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na } +| #[ polymorphic; ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na } -> { - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac } + add_inversion_lemma_exn ~poly:polymorphic na c Sorts.InProp false inv_clear_tac } END VERNAC COMMAND EXTEND DeriveInversion -| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] +| #[ polymorphic; ] [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] => { seff na } -> { - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac } + add_inversion_lemma_exn ~poly:polymorphic na c s false inv_tac } -| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na } +| #[ polymorphic; ] [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na } -> { - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac } + add_inversion_lemma_exn ~poly:polymorphic na c Sorts.InProp false inv_tac } END VERNAC COMMAND EXTEND DeriveDependentInversion -| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] +| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] => { seff na } -> { - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac } + add_inversion_lemma_exn ~poly:polymorphic na c s true dinv_tac } END VERNAC COMMAND EXTEND DeriveDependentInversionClear -| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] +| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] => { seff na } -> { - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac } + add_inversion_lemma_exn ~poly:polymorphic na c s true dinv_clear_tac } END (**********************************************************************) @@ -855,9 +849,9 @@ END TACTIC EXTEND transparent_abstract | [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } | [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } END (* ********************************************************************* *) diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index c07b653f3a..5af393a3e5 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -239,10 +239,9 @@ ARGUMENT EXTEND opthints END VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF -| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { - let open Vernacinterp in +| #[ locality = Attributes.locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints ~local:(Locality.make_section_locality atts.locality) + Hints.add_hints ~local:(Locality.make_section_locality locality) (match dbnames with None -> ["core"] | Some l -> l) entry; } END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index d62f985350..c58c8556c5 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -22,6 +22,7 @@ open Genarg open Genredexpr open Tok (* necessary for camlp5 *) open Names +open Attributes open Pcoq open Pcoq.Prim @@ -498,12 +499,12 @@ VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY { pr_ltac_production_item END VERNAC COMMAND EXTEND VernacTacticNotation -| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => +| #[ deprecation; locality; ] + [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => { VtSideff [], VtNow } -> - { let open Vernacinterp in - let n = Option.default 0 n in - let deprecation = atts.deprecated in - Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e; + { + let n = Option.default 0 n in + Tacentries.add_tactic_notation (Locality.make_module_locality locality) n ?deprecation r e; } END @@ -545,13 +546,12 @@ PRINTED BY { pr_tacdef_body } END VERNAC COMMAND EXTEND VernacDeclareTacticDefinition -| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { +| #[ deprecation; locality; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { VtSideff (List.map (function | TacticDefinition ({CAst.v=r},_) -> r | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater - } -> { let open Vernacinterp in - let deprecation = atts.deprecated in - Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l; + } -> { + Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l; } END diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 26f2b08d3a..aa78fb5d1e 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -131,10 +131,9 @@ VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF END VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF -| [ "Obligation" "Tactic" ":=" tactic(t) ] -> { - let open Vernacinterp in +| #[ locality = Attributes.locality; ] [ "Obligation" "Tactic" ":=" tactic(t) ] -> { set_default_tactic - (Locality.make_section_locality atts.locality) + (Locality.make_section_locality locality) (Tacintern.glob_tactic t); } END diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 3e47724c4c..1c7220ddc0 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -180,36 +180,36 @@ TACTIC EXTEND setoid_rewrite END VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF - | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - { declare_relation a aeq n (Some lemma1) (Some lemma2) None } + { declare_relation atts a aeq n (Some lemma1) (Some lemma2) None } - | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> - { declare_relation a aeq n (Some lemma1) None None } - | [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> - { declare_relation a aeq n None None None } + { declare_relation atts a aeq n (Some lemma1) None None } + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> + { declare_relation atts a aeq n None None None } END VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF - | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - { declare_relation a aeq n None (Some lemma2) None } - | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation a aeq n None (Some lemma2) (Some lemma3) } + { declare_relation atts a aeq n None (Some lemma2) None } + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + { declare_relation atts a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF - | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation a aeq n (Some lemma1) None (Some lemma3) } - | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + { declare_relation atts a aeq n (Some lemma1) None (Some lemma3) } + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + { declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation a aeq n None None (Some lemma3) } + { declare_relation atts a aeq n None None (Some lemma3) } END { @@ -236,64 +236,64 @@ GRAMMAR EXTEND Gram END VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - { declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None } - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None } + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> - { declare_relation ~binders:b a aeq n (Some lemma1) None None } - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> - { declare_relation ~binders:b a aeq n None None None } + { declare_relation atts ~binders:b a aeq n (Some lemma1) None None } + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> + { declare_relation atts ~binders:b a aeq n None None None } END VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - { declare_relation ~binders:b a aeq n None (Some lemma2) None } - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) } + { declare_relation atts ~binders:b a aeq n None (Some lemma2) None } + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + { declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) } - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + { declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) } + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation ~binders:b a aeq n None None (Some lemma3) } + { declare_relation atts ~binders:b a aeq n None None (Some lemma3) } END VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF - | [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - { let open Vernacinterp in - add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n; + | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + { + add_setoid atts [] a aeq t n; } - | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - { let open Vernacinterp in - add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n; + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + { + add_setoid atts binders a aeq t n; } - | [ "Add" "Morphism" constr(m) ":" ident(n) ] + | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) => { Vernacexpr.VtUnknown, Vernacexpr.VtNow } - -> { let open Vernacinterp in - add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n; + -> { + add_morphism_infer atts m n; } - | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] + | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) } - -> { let open Vernacinterp in - add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n; + -> { + add_morphism atts [] m s n; } - | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) } - -> { let open Vernacinterp in - add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n; + -> { + add_morphism atts binders m s n; } END diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 9f7669f1d5..7d917c58fe 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -43,6 +43,14 @@ module NamedDecl = Context.Named.Declaration (** Typeclass-based generalized rewriting. *) +type rewrite_attributes = { polymorphic : bool; program : bool; global : bool } + +let rewrite_attributes = + let open Attributes.Notations in + Attributes.(polymorphic ++ program ++ locality) >>= fun ((polymorphic, program), locality) -> + let global = not (Locality.make_section_locality locality) in + Attributes.Notations.return { polymorphic; program; global } + (** Constants used by the tactic. *) let classes_dirpath = @@ -1492,7 +1500,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul if not (Evd.is_defined acc ev) then user_err ~hdr:"rewrite" (str "Unsolved constraint remaining: " ++ spc () ++ - Termops.pr_evar_info (Evd.find acc ev)) + Termops.pr_evar_info env acc (Evd.find acc ev)) else Evd.remove acc ev) cstrs evars' in @@ -1776,67 +1784,65 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] -let anew_instance global binders instance fields = - let program_mode = Flags.is_program_mode () in - let poly = Flags.is_universe_polymorphism () in - new_instance ~program_mode poly +let anew_instance atts binders instance fields = + let program_mode = atts.program in + new_instance ~program_mode atts.polymorphic binders instance (Some (true, CAst.make @@ CRecord (fields))) - ~global ~generalize:false ~refine:false Hints.empty_hint_info + ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info -let declare_instance_refl global binders a aeq n lemma = +let declare_instance_refl atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" - in anew_instance global binders instance + in anew_instance atts binders instance [(qualid_of_ident (Id.of_string "reflexivity"),lemma)] -let declare_instance_sym global binders a aeq n lemma = +let declare_instance_sym atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric" - in anew_instance global binders instance + in anew_instance atts binders instance [(qualid_of_ident (Id.of_string "symmetry"),lemma)] -let declare_instance_trans global binders a aeq n lemma = +let declare_instance_trans atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive" - in anew_instance global binders instance + in anew_instance atts binders instance [(qualid_of_ident (Id.of_string "transitivity"),lemma)] -let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = +let declare_relation atts ?(binders=[]) a aeq n refl symm trans = init_setoid (); - let global = not (Locality.make_section_locality locality) in let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" - in ignore(anew_instance global binders instance []); + in ignore(anew_instance atts binders instance []); match (refl,symm,trans) with (None, None, None) -> () | (Some lemma1, None, None) -> - ignore (declare_instance_refl global binders a aeq n lemma1) + ignore (declare_instance_refl atts binders a aeq n lemma1) | (None, Some lemma2, None) -> - ignore (declare_instance_sym global binders a aeq n lemma2) + ignore (declare_instance_sym atts binders a aeq n lemma2) | (None, None, Some lemma3) -> - ignore (declare_instance_trans global binders a aeq n lemma3) + ignore (declare_instance_trans atts binders a aeq n lemma3) | (Some lemma1, Some lemma2, None) -> - ignore (declare_instance_refl global binders a aeq n lemma1); - ignore (declare_instance_sym global binders a aeq n lemma2) + ignore (declare_instance_refl atts binders a aeq n lemma1); + ignore (declare_instance_sym atts binders a aeq n lemma2) | (Some lemma1, None, Some lemma3) -> - let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in - let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in + let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in + let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in ignore( - anew_instance global binders instance + anew_instance atts binders instance [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1); (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]) | (None, Some lemma2, Some lemma3) -> - let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in - let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in + let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in + let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in ignore( - anew_instance global binders instance + anew_instance atts binders instance [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2); (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]) | (Some lemma1, Some lemma2, Some lemma3) -> - let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in - let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in - let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in + let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in + let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in + let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( - anew_instance global binders instance + anew_instance atts binders instance [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1); (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2); (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]) @@ -1935,15 +1941,15 @@ let warn_add_setoid_deprecated = CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () -> Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation.")) -let add_setoid global binders a aeq t n = +let add_setoid atts binders a aeq t n = warn_add_setoid_deprecated ?loc:a.CAst.loc (); init_setoid (); - let _lemma_refl = declare_instance_refl global binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in - let _lemma_sym = declare_instance_sym global binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in - let _lemma_trans = declare_instance_trans global binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in + let _lemma_refl = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in + let _lemma_sym = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in + let _lemma_trans = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( - anew_instance global binders instance + anew_instance atts binders instance [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) @@ -1958,26 +1964,26 @@ let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id")) -let add_morphism_infer glob m n = +let add_morphism_infer atts m n = warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); - let poly = Flags.is_universe_polymorphism () in + (* NB: atts.program is ignored, program mode automatically set by vernacentries *) let instance_id = add_suffix n "_Proper" in let env = Global.env () in let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in if Lib.is_modtype () then - let uctx = UState.const_univ_entry ~poly uctx in + let uctx = UState.const_univ_entry ~poly:atts.polymorphic uctx in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry (None,(instance,uctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob (ConstRef cst)); + (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst)); declare_projection n instance_id (ConstRef cst) else - let kind = Decl_kinds.Global, poly, + let kind = Decl_kinds.Global, atts.polymorphic, Decl_kinds.DefinitionBody Decl_kinds.Instance in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in @@ -1985,7 +1991,7 @@ let add_morphism_infer glob m n = | Globnames.ConstRef cst -> add_instance (Typeclasses.new_instance (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info - glob (ConstRef cst)); + atts.global (ConstRef cst)); declare_projection n instance_id (ConstRef cst) | _ -> assert false in @@ -1995,9 +2001,8 @@ let add_morphism_infer glob m n = Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) hook; ignore (Pfedit.by (Tacinterp.interp tac))) () -let add_morphism glob binders m s n = +let add_morphism atts binders m s n = init_setoid (); - let poly = Flags.is_universe_polymorphism () in let instance_id = add_suffix n "_Proper" in let instance = (((CAst.make @@ Name instance_id),None), Explicit, @@ -2006,8 +2011,7 @@ let add_morphism glob binders m s n = [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - let program_mode = Flags.is_program_mode () in - ignore(new_instance ~program_mode ~global:glob poly binders instance + ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance (Some (true, CAst.make @@ CRecord [])) ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 0d014a0bf3..4f46e78c71 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -19,6 +19,9 @@ open Tacinterp (** TODO: document and clean me! *) +type rewrite_attributes +val rewrite_attributes : rewrite_attributes Attributes.attribute + type unary_strategy = Subterms | Subterm | Innermost | Outermost | Bottomup | Topdown | Progress | Try | Any | Repeat @@ -77,18 +80,18 @@ val cl_rewrite_clause : val is_applied_rewrite_relation : env -> evar_map -> rel_context -> constr -> types option -val declare_relation : ?locality:bool -> +val declare_relation : rewrite_attributes -> ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> constr_expr option -> constr_expr option -> constr_expr option -> unit val add_setoid : - bool -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr -> + rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr -> Id.t -> unit -val add_morphism_infer : bool -> constr_expr -> Id.t -> unit +val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> unit val add_morphism : - bool -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit + rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 16cff420bd..0f88734caf 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -353,7 +353,7 @@ let extend_atomic_tactic name entries = let default = epsilon_value inj e in match default with | None -> raise NonEmptyArgument - | Some def -> Tacintern.intern_tactic_or_tacarg Tacintern.fully_empty_glob_sign def + | Some def -> Tacintern.intern_tactic_or_tacarg (Genintern.empty_glob_sign Environ.empty_env) def in try Some (hd, List.map empty_value rem) with NonEmptyArgument -> None in diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 5b4bedb50a..c93d6251e0 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -12,7 +12,7 @@ open Vernacexpr open Tacexpr -open Vernacinterp +open Attributes (** {5 Tactic Definitions} *) diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index a88285c9ee..d5f22b2c72 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -55,7 +55,7 @@ type alias = KerName.t type alias_tactic = { alias_args: Id.t list; alias_body: glob_tactic_expr; - alias_deprecation: Vernacinterp.deprecation option; + alias_deprecation: Attributes.deprecation option; } let alias_map = Summary.ref ~name:"tactic-alias" @@ -121,7 +121,7 @@ type ltac_entry = { tac_for_ml : bool; tac_body : glob_tactic_expr; tac_redef : ModPath.t list; - tac_deprecation : Vernacinterp.deprecation option + tac_deprecation : Attributes.deprecation option } let mactab = @@ -178,7 +178,7 @@ let subst_md (subst, (local, id, b, t, deprecation)) = let classify_md (local, _, _, _, _ as o) = Substitute o let inMD : bool * ltac_constant option * bool * glob_tactic_expr * - Vernacinterp.deprecation option -> obj = + Attributes.deprecation option -> obj = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index d5d36c97fa..5b98daf383 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -12,7 +12,7 @@ open Names open Libnames open Tacexpr open Geninterp -open Vernacinterp +open Attributes (** This module centralizes the various ways of registering tactics. *) @@ -33,7 +33,7 @@ type alias = KerName.t type alias_tactic = { alias_args: Id.t list; alias_body: glob_tactic_expr; - alias_deprecation: Vernacinterp.deprecation option; + alias_deprecation: deprecation option; } (** Contents of a tactic notation *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 55412c74bb..ebec3c887c 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -44,9 +44,9 @@ type glob_sign = Genintern.glob_sign = { (* ltac variables and the subset of vars introduced by Intro/Let/... *) genv : Environ.env; extra : Genintern.Store.t; + intern_sign : Genintern.intern_variable_status; } -let fully_empty_glob_sign = Genintern.empty_glob_sign Environ.empty_env let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ()) (* We have identifier <| global_reference <| constr *) @@ -83,7 +83,8 @@ let intern_hyp ist ({loc;v=id} as locid) = else if find_ident id ist then make id else - Pretype_errors.error_var_not_found ?loc id + CErrors.user_err ?loc Pp.(str "Hypothesis" ++ spc () ++ Id.print id ++ spc() ++ + str "was not found in the current environment.") let intern_or_var f ist = function | ArgVar locid -> ArgVar (intern_hyp ist locid) @@ -121,15 +122,15 @@ let warn_deprecated_tactic = CWarnings.create ~name:"deprecated-tactic" ~category:"deprecated" (fun (qid,depr) -> str "Tactic " ++ pr_qualid qid ++ strbrk " is deprecated" ++ - pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++ - str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note) + pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++ + str "." ++ pr_opt (fun note -> str note) depr.Attributes.note) let warn_deprecated_alias = CWarnings.create ~name:"deprecated-tactic-notation" ~category:"deprecated" (fun (kn,depr) -> str "Tactic Notation " ++ Pptactic.pr_alias_key kn ++ strbrk " is deprecated since" ++ - pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++ - str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note) + pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++ + str "." ++ pr_opt (fun note -> str note) depr.Attributes.note) let intern_isolated_global_tactic_reference qid = let loc = qid.CAst.loc in @@ -209,7 +210,7 @@ let intern_binding_name ist x = and if a term w/o ltac vars, check the name is indeed quantified *) x -let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c = +let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra; intern_sign} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in let ltacvars = { @@ -218,7 +219,7 @@ let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c = ltac_extra = extra; } in let c' = - warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env Evd.(from_env env)) c + warn (Constrintern.intern_core scope ~pattern_mode ~ltacvars env Evd.(from_env env) intern_sign) c in (c',if !strict_check then None else Some c) diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 9146fced2d..178f6af71d 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -21,12 +21,11 @@ type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; genv : Environ.env; extra : Genintern.Store.t; + intern_sign : Genintern.intern_variable_status; } -val fully_empty_glob_sign : glob_sign - val make_empty_glob_sign : unit -> glob_sign - (** same as [fully_empty_glob_sign], but with [Global.env()] as + (** build an empty [glob_sign] using [Global.env()] as environment *) (** Main globalization functions *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index b60b77595b..2a046a3e65 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -686,7 +686,7 @@ let interp_may_eval f ist env sigma = function | ConstrContext ({loc;v=s},c) -> (try let (sigma,ic) = f ist env sigma c in - let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in + let ctxt = try_interp_ltac_var coerce_to_constr_context ist (Some (env, sigma)) (make ?loc s) in let ctxt = EConstr.Unsafe.to_constr ctxt in let ic = EConstr.Unsafe.to_constr ic in let c = subst_meta [Constr_matching.special_meta,ic] ctxt in @@ -1078,7 +1078,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with push_trace(None,call) ist >>= fun trace -> Profile_ltac.do_profile "eval_tactic:TacAbstract" trace (catch_error_tac trace begin - Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT + Proofview.Goal.enter begin fun gl -> Abstract.tclABSTRACT (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t) end end) | TacThen (t1,t) -> @@ -2024,7 +2024,7 @@ let interp_ltac_constr ist c k = Ftactic.run (interp_ltac_constr ist c) k let interp_redexp env sigma r = let ist = default_ist () in - let gist = { fully_empty_glob_sign with genv = env; } in + let gist = Genintern.empty_glob_sign env in interp_red_expr ist env sigma (intern_red_expr gist r) (***************************************************************************) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index a284c3bfc7..5d75b28539 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -940,7 +940,7 @@ let pf_saturate ?beta ?bi_types gl c ?ty m = let pf_partial_solution gl t evl = let sigma, g = project gl, sig_it gl in - let sigma = Goal.V82.partial_solution sigma g t in + let sigma = Goal.V82.partial_solution (pf_env gl) sigma g t in re_sig (List.map (fun x -> (fst (EConstr.destEvar sigma x))) evl) sigma let dependent_apply_error = diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index c04ced4ab4..036b20bfcd 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -433,15 +433,15 @@ let lz_coq_prod = let lz_setoid_relation = let sdir = ["Classes"; "RelationClasses"] in - let last_srel = ref (Environ.empty_env, None) in + let last_srel = ref None in fun env -> match !last_srel with - | env', srel when env' == env -> srel + | Some (env', srel) when env' == env -> srel | _ -> let srel = try Some (UnivGen.constr_of_global @@ Coqlib.find_reference "Class_setoid" ("Coq"::sdir) "RewriteRelation" [@ocaml.warning "-3"]) with _ -> None in - last_srel := (env, srel); srel + last_srel := Some (env, srel); srel let ssr_is_setoid env = match lz_setoid_relation env with diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 940defb743..4ed75cdbe4 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -170,10 +170,9 @@ let declare_one_prenex_implicit locality f = } VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF - | [ "Prenex" "Implicits" ne_global_list(fl) ] + | #[ locality = Attributes.locality; ] [ "Prenex" "Implicits" ne_global_list(fl) ] -> { - let open Vernacinterp in - let locality = Locality.make_section_locality atts.locality in + let locality = Locality.make_section_locality locality in List.iter (declare_one_prenex_implicit locality) fl; } END diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 7f67487f5d..bb6decd848 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -1048,7 +1048,7 @@ let thin id sigma goal = | None -> sigma | Some (sigma, hyps, concl) -> let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl in - let sigma = Goal.V82.partial_solution_to sigma goal gl ev in + let sigma = Goal.V82.partial_solution_to env sigma goal gl ev in sigma (* diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index 5dbc9eea7a..13e0bcbd47 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -16,7 +16,6 @@ open Notation open Numeral open Pp open Names -open Vernacinterp open Ltac_plugin open Stdarg open Pcoq.Prim @@ -36,7 +35,7 @@ ARGUMENT EXTEND numnotoption END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF - | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(o) ] -> - { vernac_numeral_notation (Locality.make_module_locality atts.locality) ty f g (Id.to_string sc) o } + { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } END |