diff options
Diffstat (limited to 'plugins/ltac')
46 files changed, 174 insertions, 153 deletions
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index d9338f0421..2159c05f80 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -150,7 +150,7 @@ TACTIC EXTEND specialize | [ "specialize" constr_with_bindings(c) ] -> { Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None) } -| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> { +| [ "specialize" constr_with_bindings(c) "as" simple_intropattern(ipat) ] -> { Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat)) } END diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 050fdcb608..5211bedd46 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/evar_tactics.mli b/plugins/ltac/evar_tactics.mli index b6cfc38260..d99c800320 100644 --- a/plugins/ltac/evar_tactics.mli +++ b/plugins/ltac/evar_tactics.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index eb9cacb975..2654729652 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -35,7 +35,7 @@ let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Stdarg.wit_constr -let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_intro_pattern +let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_simple_intropattern let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr let () = let inject (loc, v) = Tacexpr.Tacexp v in @@ -46,7 +46,7 @@ let () = let () = let register name entry = Tacentries.register_tactic_notation_entry name entry in register "hyp" wit_var; - register "simple_intropattern" wit_intro_pattern; + register "simple_intropattern" wit_simple_intropattern; register "integer" wit_integer; register "reference" wit_ref; () diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 7f9eecbef5..6dd51e4e01 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 7691ca225e..1e2b23bf96 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -174,15 +174,15 @@ TACTIC EXTEND einjection | [ "einjection" destruction_arg(c) ] -> { mytclWithHoles (injClause None None) true c } END TACTIC EXTEND injection_as -| [ "injection" "as" intropattern_list(ipat)] -> +| [ "injection" "as" simple_intropattern_list(ipat)] -> { injClause None (Some (decode_inj_ipat ipat)) false None } -| [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] -> +| [ "injection" destruction_arg(c) "as" simple_intropattern_list(ipat)] -> { mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) false c } END TACTIC EXTEND einjection_as -| [ "einjection" "as" intropattern_list(ipat)] -> +| [ "einjection" "as" simple_intropattern_list(ipat)] -> { injClause None (Some (decode_inj_ipat ipat)) true None } -| [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] -> +| [ "einjection" destruction_arg(c) "as" simple_intropattern_list(ipat)] -> { mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) true c } END TACTIC EXTEND simple_injection @@ -328,7 +328,7 @@ let add_rewrite_hint ~poly bases ort t lcsr = if poly then ctx else (* This is a global universe context that shouldn't be refreshed at every use of the hint, declare it globally. *) - (Declare.declare_universe_context false ctx; + (Declare.declare_universe_context ~poly:false ctx; Univ.ContextSet.empty) in CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in @@ -336,7 +336,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 _ = VtSideff [], VtLater +let classify_hint _ = VtSideff ([], VtLater) } @@ -422,7 +422,7 @@ END open Inv open Leminv -let seff id = VtSideff [id], VtLater +let seff id = VtSideff ([id], VtLater) } diff --git a/plugins/ltac/extratactics.mli b/plugins/ltac/extratactics.mli index 4576562634..e47226410a 100644 --- a/plugins/ltac/extratactics.mli +++ b/plugins/ltac/extratactics.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index e59076bd63..8344f9dae3 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 049a699cbd..0aaf417f33 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/g_eqdecide.mlg b/plugins/ltac/g_eqdecide.mlg index e57afe3e33..d416f08c06 100644 --- a/plugins/ltac/g_eqdecide.mlg +++ b/plugins/ltac/g_eqdecide.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index d10d10a664..5c84b35f1b 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -38,7 +38,7 @@ let arg_of_expr = function let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n -let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat +let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_simple_intropattern) pat let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac @@ -446,8 +446,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve STATE proof let solving_tac = is_explicit_terminator t in let parallel = `Yes (solving_tac,anon_abstracting_tac) in let pbr = if solving_tac then Some "par" else None in - VtProofStep{ parallel = parallel; proof_block_detection = pbr }, - VtLater + VtProofStep{ parallel = parallel; proof_block_detection = pbr } } -> { let t = rm_abstract t in vernac_solve Goal_select.SelectAll n t def @@ -494,7 +493,7 @@ END VERNAC COMMAND EXTEND VernacTacticNotation | #[ deprecation; locality; ] [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => - { VtSideff [], VtNow } -> + { VtSideff ([], VtNow) } -> { let n = Option.default 0 n in Tacentries.add_tactic_notation (Locality.make_module_locality locality) n ?deprecation r e; @@ -542,7 +541,7 @@ VERNAC COMMAND EXTEND VernacDeclareTacticDefinition | #[ 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 + | TacticRedefinition (qid,_) -> qualid_basename qid) l, VtLater) } -> { Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l; } diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 58c8dabd79..455c8ab003 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -83,7 +83,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 _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater) +let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[])) } diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 1a84158df7..d25448b5cb 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -277,19 +277,19 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF add_setoid atts binders a aeq t n } | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] - => { VtStartProof(GuaranteesOpacity, [n]), VtLater } + => { VtStartProof(GuaranteesOpacity, [n]) } -> { if Lib.is_modtype () then CErrors.user_err Pp.(str "Add Morphism cannot be used in a module type. Use Parameter Morphism instead."); add_morphism_interactive atts m n } | #[ atts = rewrite_attributes; ] [ "Declare" "Morphism" constr(m) ":" ident(n) ] - => { VtSideff([n]), VtLater } + => { VtSideff([n], VtLater) } -> { add_morphism_as_parameter atts m n } | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => { VtStartProof(GuaranteesOpacity,[n]), VtLater } + => { VtStartProof(GuaranteesOpacity,[n]) } -> { add_morphism atts [] m s n } | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => { VtStartProof(GuaranteesOpacity,[n]), VtLater } + => { VtStartProof(GuaranteesOpacity,[n]) } -> { add_morphism atts binders m s n } END diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index c23240b782..945a2dd613 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 759bb62fdd..e3042dc3cb 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -52,7 +52,9 @@ let () = let open Stdarg in let open Tacarg in register_grammar wit_int_or_var (int_or_var); - register_grammar wit_intro_pattern (simple_intropattern); + register_grammar wit_intro_pattern (simple_intropattern); (* To remove at end of deprecation phase *) +(* register_grammar wit_intropattern (intropattern); *) (* To be added at end of deprecation phase *) + register_grammar wit_simple_intropattern (simple_intropattern); register_grammar wit_quant_hyp (quantified_hypothesis); register_grammar wit_uconstr (uconstr); register_grammar wit_open_constr (open_constr); diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 9bff98b6c3..aa2631ae41 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 79f0f521cc..db8d09b79e 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -1314,6 +1314,12 @@ let pr_glob_constr_pptac env sigma c = let pr_lglob_constr_pptac env sigma c = pr_lglob_constr_env env c +let pr_raw_intro_pattern = + lift_env (fun env sigma -> Miscprint.pr_intro_pattern @@ pr_constr_expr env sigma) + +let pr_glob_intro_pattern = + lift_env (fun env sigma -> Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac env sigma c)) + let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in @@ -1323,11 +1329,8 @@ let () = pr_qualid (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; register_basic_print0 wit_var pr_lident pr_lident pr_id; - register_print0 - wit_intro_pattern - (lift_env (fun env sigma -> Miscprint.pr_intro_pattern @@ pr_constr_expr env sigma)) - (lift_env (fun env sigma -> Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac env sigma c))) - pr_intro_pattern_env; + register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"]; + register_print0 wit_simple_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl (lift (pr_clauses (Some true) pr_lident)) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 70af09833d..9cff3ea1eb 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index ae4b53325f..243e0e945c 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli index 6a67aab5dc..7595f53fd7 100644 --- a/plugins/ltac/profile_ltac.mli +++ b/plugins/ltac/profile_ltac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/profile_ltac_tactics.mlg b/plugins/ltac/profile_ltac_tactics.mlg index 2713819c7b..9dd71505c8 100644 --- a/plugins/ltac/profile_ltac_tactics.mlg +++ b/plugins/ltac/profile_ltac_tactics.mlg @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2da6584aba..13844c2707 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -1795,7 +1795,7 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance atts binders (name,t) fields = - let _id = Classes.new_instance atts.polymorphic + let _id = Classes.new_instance ~poly:atts.polymorphic name binders t (true, CAst.make @@ CRecord (fields)) ~global:atts.global ~generalize:false Hints.empty_hint_info in @@ -1898,11 +1898,11 @@ let declare_projection n instance_id r = let univs = Evd.univ_entry ~poly sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in - let cst = - Declare.definition_entry ~types:typ ~univs term - in - ignore(Declare.declare_constant n - (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) + let cst = Declare.definition_entry ~types:typ ~univs term in + let _ : Constant.t = + Declare.declare_constant ~name:n ~kind:Decls.(IsDefinition Definition) + (Declare.DefinitionEntry cst) + in () let build_morphism_signature env sigma m = let m,ctx = Constrintern.interp_constr env sigma m in @@ -1978,10 +1978,9 @@ let add_morphism_as_parameter atts m n : unit = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in let uctx = UState.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) + let cst = Declare.declare_constant ~name:instance_id + ~kind:Decls.(IsAssumption Logical) + (Declare.ParameterEntry (None,(instance,uctx),None)) in Classes.add_instance (Classes.mk_instance (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); @@ -1994,11 +1993,10 @@ let add_morphism_interactive atts m n : Lemmas.t = let env = Global.env () in let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in - let kind = Decl_kinds.Global Decl_kinds.ImportDefaultBehavior, atts.polymorphic, - Decl_kinds.DefinitionBody Decl_kinds.Instance - in + let poly = atts.polymorphic in + let kind = Decls.(IsDefinition Instance) in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in - let hook _ _ _ = function + let hook { DeclareDef.Hook.S.dref; _ } = dref |> function | Globnames.ConstRef cst -> Classes.add_instance (Classes.mk_instance (PropGlobal.proper_class env evd) Hints.empty_hint_info @@ -2006,10 +2004,11 @@ let add_morphism_interactive atts m n : Lemmas.t = declare_projection n instance_id (ConstRef cst) | _ -> assert false in - let hook = Lemmas.mk_hook hook in + let hook = DeclareDef.Hook.make hook in + let info = Lemmas.Info.make ~hook ~kind () in Flags.silently (fun () -> - let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in + let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in fst (Lemmas.by (Tacinterp.interp tac) lemma)) () let add_morphism atts binders m s n = @@ -2023,7 +2022,7 @@ let add_morphism atts binders m s n = in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in let _id, lemma = Classes.new_instance_interactive - ~global:atts.global atts.polymorphic + ~global:atts.global ~poly:atts.polymorphic instance_name binders instance_t ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index a5c3782b30..8e0b0a8003 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index 8a25d4851f..9e8e86d4fc 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -19,13 +19,19 @@ let make0 ?dyn name = let () = Geninterp.register_val0 wit dyn in wit -let wit_intro_pattern = make0 "intropattern" +let wit_intropattern = make0 "intropattern" (* To keep after deprecation phase but it will get a different parsing semantics (Tactic Notation and TACTIC EXTEND) in pltac.ml *) +let wit_simple_intropattern = make0 "simple_intropattern" let wit_quant_hyp = make0 "quant_hyp" let wit_constr_with_bindings = make0 "constr_with_bindings" let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" let wit_bindings = make0 "bindings" let wit_quantified_hypothesis = wit_quant_hyp -let wit_intropattern = wit_intro_pattern + +(* A convenient common part to simple_intropattern and intropattern + usable when no parsing rule is concerned: indeed + simple_intropattern and intropattern are in the same type and have + the same interp/intern/subst methods *) +let wit_intro_pattern = wit_intropattern let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = make0 "tactic" diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index 0c7096a4de..945f237c91 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -16,6 +16,12 @@ open Tactypes open Tacexpr (** Tactic related witnesses, could also live in tactics/ if other users *) +(* To keep after deprecation phase but it will get a different parsing semantics in pltac.ml *) +val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type +[@@ocaml.deprecated "Use wit_simple_intropattern"] + +val wit_simple_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type + val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type val wit_quant_hyp : quantified_hypothesis uniform_genarg_type @@ -36,7 +42,6 @@ val wit_bindings : constr bindings delayed_open) genarg_type val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type -val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type (** Generic arguments based on Ltac. *) diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index fcab98c7e8..4e79bab28e 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -144,9 +144,22 @@ let coerce_to_constr_context v = out_gen (topwit wit_constr_context) v else raise (CannotCoerceTo "a term context") +let is_intro_pattern v = + if has_type v (topwit wit_intropattern [@warning "-3"]) then + Some (out_gen (topwit wit_intropattern [@warning "-3"]) v).CAst.v + else + if has_type v (topwit wit_simple_intropattern) then + Some (out_gen (topwit wit_simple_intropattern) v).CAst.v + else + None + (* Interprets an identifier which must be fresh *) let coerce_var_to_ident fresh env sigma v = let fail () = raise (CannotCoerceTo "a fresh identifier") in + match is_intro_pattern v with + | Some (IntroNaming (IntroIdentifier id)) -> id + | Some _ -> fail () + | None -> if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with | { CAst.v=IntroNaming (IntroIdentifier id)} -> id @@ -170,11 +183,11 @@ let id_of_name = function | Name.Anonymous -> Id.of_string "x" | Name.Name x -> x in let fail () = raise (CannotCoerceTo "an identifier") in - if has_type v (topwit wit_intro_pattern) then - match out_gen (topwit wit_intro_pattern) v with - | {CAst.v=IntroNaming (IntroIdentifier id)} -> id - | _ -> fail () - else if has_type v (topwit wit_var) then + match is_intro_pattern v with + | Some (IntroNaming (IntroIdentifier id)) -> id + | Some _ -> fail () + | None -> + if has_type v (topwit wit_var) then out_gen (topwit wit_var) v else match Value.to_constr v with @@ -209,9 +222,10 @@ let id_of_name = function let coerce_to_intro_pattern sigma v = - if has_type v (topwit wit_intro_pattern) then - (out_gen (topwit wit_intro_pattern) v).CAst.v - else if has_type v (topwit wit_var) then + match is_intro_pattern v with + | Some pat -> pat + | None -> + if has_type v (topwit wit_var) then let id = out_gen (topwit wit_var) v in IntroNaming (IntroIdentifier id) else match Value.to_constr v with @@ -227,11 +241,9 @@ let coerce_to_intro_pattern_naming sigma v = | _ -> raise (CannotCoerceTo "a naming introduction pattern") let coerce_to_hint_base v = - if has_type v (topwit wit_intro_pattern) then - match out_gen (topwit wit_intro_pattern) v with - | {CAst.v=IntroNaming (IntroIdentifier id)} -> Id.to_string id - | _ -> raise (CannotCoerceTo "a hint base name") - else raise (CannotCoerceTo "a hint base name") + match is_intro_pattern v with + | Some (IntroNaming (IntroIdentifier id)) -> Id.to_string id + | Some _ | None -> raise (CannotCoerceTo "a hint base name") let coerce_to_int v = if has_type v (topwit wit_int) then @@ -240,12 +252,12 @@ let coerce_to_int v = let coerce_to_constr env v = let fail () = raise (CannotCoerceTo "a term") in - if has_type v (topwit wit_intro_pattern) then - match out_gen (topwit wit_intro_pattern) v with - | {CAst.v=IntroNaming (IntroIdentifier id)} -> + match is_intro_pattern v with + | Some (IntroNaming (IntroIdentifier id)) -> (try ([], constr_of_id env id) with Not_found -> fail ()) - | _ -> fail () - else if has_type v (topwit wit_constr) then + | Some _ -> fail () + | None -> + if has_type v (topwit wit_constr) then let c = out_gen (topwit wit_constr) v in ([], c) else if has_type v (topwit wit_constr_under_binders) then @@ -269,11 +281,11 @@ let coerce_to_closed_constr env v = let coerce_to_evaluable_ref env sigma v = let fail () = raise (CannotCoerceTo "an evaluable reference") in let ev = - if has_type v (topwit wit_intro_pattern) then - match out_gen (topwit wit_intro_pattern) v with - | {CAst.v=IntroNaming (IntroIdentifier id)} when is_variable env id -> EvalVarRef id - | _ -> fail () - else if has_type v (topwit wit_var) then + match is_intro_pattern v with + | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> EvalVarRef id + | Some _ -> fail () + | None -> + if has_type v (topwit wit_var) then let id = out_gen (topwit wit_var) v in if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id else fail () @@ -308,11 +320,11 @@ let coerce_to_intro_pattern_list ?loc sigma v = let coerce_to_hyp env sigma v = let fail () = raise (CannotCoerceTo "a variable") in - if has_type v (topwit wit_intro_pattern) then - match out_gen (topwit wit_intro_pattern) v with - | {CAst.v=IntroNaming (IntroIdentifier id)} when is_variable env id -> id - | _ -> fail () - else if has_type v (topwit wit_var) then + match is_intro_pattern v with + | Some (IntroNaming (IntroIdentifier id)) when is_variable env id -> id + | Some _ -> fail () + | None -> + if has_type v (topwit wit_var) then let id = out_gen (topwit wit_var) v in if is_variable env id then id else fail () else match Value.to_constr v with @@ -340,12 +352,11 @@ let coerce_to_reference sigma v = (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) let coerce_to_quantified_hypothesis sigma v = - if has_type v (topwit wit_intro_pattern) then - let v = out_gen (topwit wit_intro_pattern) v in - match v with - | {CAst.v=IntroNaming (IntroIdentifier id)} -> NamedHyp id - | _ -> raise (CannotCoerceTo "a quantified hypothesis") - else if has_type v (topwit wit_var) then + match is_intro_pattern v with + | Some (IntroNaming (IntroIdentifier id)) -> NamedHyp id + | Some _ -> raise (CannotCoerceTo "a quantified hypothesis") + | None -> + if has_type v (topwit wit_var) then let id = out_gen (topwit wit_var) v in NamedHyp id else if has_type v (topwit wit_int) then diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index b04c3b9f4e..22d1681a61 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 814be64f81..13a2f3b8c0 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 309db539d0..95b958955e 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -12,11 +12,10 @@ open Vernacexpr open Tacexpr -open Attributes (** {5 Tactic Definitions} *) -val register_ltac : locality_flag -> ?deprecation:deprecation -> +val register_ltac : locality_flag -> ?deprecation:Deprecation.t -> Tacexpr.tacdef_body list -> unit (** Adds new Ltac definitions to the environment. *) @@ -36,7 +35,7 @@ type argument = Genarg.ArgT.any Extend.user_symbol leaves. *) val add_tactic_notation : - locality_flag -> int -> ?deprecation:deprecation -> raw_argument + locality_flag -> int -> ?deprecation:Deprecation.t -> raw_argument grammar_tactic_prod_item_expr list -> raw_tactic_expr -> unit (** [add_tactic_notation local level prods expr] adds a tactic notation in the environment at level [level] with locality [local] made of the grammar @@ -49,7 +48,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type - to finding an argument by name (as in {!Genarg}) if there is none matching. *) -val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:deprecation -> +val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:Deprecation.t -> argument grammar_tactic_prod_item_expr list list -> unit (** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND ML-side macro. *) @@ -80,7 +79,7 @@ type _ ty_sig = type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml val tactic_extend : string -> string -> level:Int.t -> - ?deprecation:deprecation -> ty_ml list -> unit + ?deprecation:Deprecation.t -> ty_ml list -> unit (** {5 ARGUMENT EXTEND} *) diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index d5f22b2c72..6a5ab55604 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -55,7 +55,7 @@ type alias = KerName.t type alias_tactic = { alias_args: Id.t list; alias_body: glob_tactic_expr; - alias_deprecation: Attributes.deprecation option; + alias_deprecation: Deprecation.t 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 : Attributes.deprecation option + tac_deprecation : Deprecation.t 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 * - Attributes.deprecation option -> obj = + Deprecation.t 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 5b98daf383..6a1e6e3bbd 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -12,7 +12,6 @@ open Names open Libnames open Tacexpr open Geninterp -open Attributes (** This module centralizes the various ways of registering tactics. *) @@ -33,7 +32,7 @@ type alias = KerName.t type alias_tactic = { alias_args: Id.t list; alias_body: glob_tactic_expr; - alias_deprecation: deprecation option; + alias_deprecation: Deprecation.t option; } (** Contents of a tactic notation *) @@ -48,7 +47,7 @@ val check_alias : alias -> bool (** {5 Coq tactic definitions} *) -val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t -> +val register_ltac : bool -> bool -> ?deprecation:Deprecation.t -> Id.t -> glob_tactic_expr -> unit (** Register a new Ltac with the given name and body. @@ -57,7 +56,7 @@ val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t -> definition. It also puts the Ltac name in the nametab, so that it can be used unqualified. *) -val redefine_ltac : bool -> ?deprecation:deprecation -> KerName.t -> +val redefine_ltac : bool -> ?deprecation:Deprecation.t -> KerName.t -> glob_tactic_expr -> unit (** Replace a Ltac with the given name and body. If the boolean flag is set to true, then this is a local redefinition. *) @@ -68,7 +67,7 @@ val interp_ltac : KerName.t -> glob_tactic_expr val is_ltac_for_ml_tactic : KerName.t -> bool (** Whether the tactic is defined from ML-side *) -val tac_deprecation : KerName.t -> deprecation option +val tac_deprecation : KerName.t -> Deprecation.t option (** The tactic deprecation notice, if any *) type ltac_entry = { @@ -78,7 +77,7 @@ type ltac_entry = { (** The current body of the tactic *) tac_redef : ModPath.t list; (** List of modules redefining the tactic in reverse chronological order *) - tac_deprecation : deprecation option; + tac_deprecation : Deprecation.t option; (** Deprecation notice to be printed when the tactic is used *) } diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 8bd69dd4fd..e6e0c9d92c 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index f839c3e886..6abcdf2afa 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index c1f7fab123..3ed5b1aab2 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -119,18 +119,13 @@ let intern_constr_reference strict ist qid = (* Internalize an isolated reference in position of tactic *) 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.Attributes.since ++ - str "." ++ pr_opt (fun note -> str note) depr.Attributes.note) + Deprecation.create_warning ~object_name:"Tactic" ~warning_name:"deprecated-tactic" + pr_qualid 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.Attributes.since ++ - str "." ++ pr_opt (fun note -> str note) depr.Attributes.note) + Deprecation.create_warning ~object_name:"Tactic Notation" + ~warning_name:"deprecated-tactic-notation" + Pptactic.pr_alias_key let intern_isolated_global_tactic_reference qid = let loc = qid.CAst.loc in @@ -800,7 +795,8 @@ let () = let ist = { ist with ltacvars = !lf } in (ist, ans) in - Genintern.register_intern0 wit_intro_pattern intern_intro_pattern + Genintern.register_intern0 wit_intropattern intern_intro_pattern [@warning "-3"]; + Genintern.register_intern0 wit_simple_intropattern intern_intro_pattern let () = let intern_clause ist cl = diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 978ad4dd24..0480b0c34d 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 4a0b01bcdc..8ddf17ca14 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -2029,7 +2029,8 @@ let () = register_interp0 wit_pre_ident (lift interp_pre_ident); register_interp0 wit_ident (lift interp_ident); register_interp0 wit_var (lift interp_hyp); - register_interp0 wit_intro_pattern (lifts interp_intro_pattern); + register_interp0 wit_intropattern (lifts interp_intro_pattern) [@warning "-3"]; + register_interp0 wit_simple_intropattern (lifts interp_intro_pattern); register_interp0 wit_clause_dft_concl (lift interp_clause); register_interp0 wit_constr (lifts interp_constr); register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v); diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 22a092fa8b..c7c30bc167 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index a3eeca2267..b6e7dd64b0 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -287,7 +287,8 @@ let () = Genintern.register_subst0 wit_pre_ident (fun _ v -> v); Genintern.register_subst0 wit_ident (fun _ v -> v); Genintern.register_subst0 wit_var (fun _ v -> v); - Genintern.register_subst0 wit_intro_pattern (fun _ v -> v); + Genintern.register_subst0 wit_intropattern subst_intro_pattern [@warning "-3"]; + Genintern.register_subst0 wit_simple_intropattern subst_intro_pattern; Genintern.register_subst0 wit_tactic subst_tactic; Genintern.register_subst0 wit_ltac subst_tactic; Genintern.register_subst0 wit_constr subst_glob_constr; diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli index 4487604dca..00b148166a 100644 --- a/plugins/ltac/tacsubst.mli +++ b/plugins/ltac/tacsubst.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 04f3116664..3014ba5115 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 74ea4e6b74..e0126ad448 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 7783661787..d008f9da1f 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli index 457c4e0b9a..b847ebbc66 100644 --- a/plugins/ltac/tactic_matching.mli +++ b/plugins/ltac/tactic_matching.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml index f6b2e5b362..21e02d4c04 100644 --- a/plugins/ltac/tactic_option.ml +++ b/plugins/ltac/tactic_option.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/tactic_option.mli b/plugins/ltac/tactic_option.mli index d2f2947c94..637dd238fe 100644 --- a/plugins/ltac/tactic_option.mli +++ b/plugins/ltac/tactic_option.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index d1951cc18d..94af4a3151 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) |