diff options
Diffstat (limited to 'plugins/ltac')
46 files changed, 371 insertions, 319 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 f5098d2a34..49d8ab4e23 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 *) @@ -146,6 +146,23 @@ let discrHyp id = let injection_main with_evars c = elimOnConstrWithHoles (injClause None None) with_evars c +let isInjPat pat = match pat.CAst.v with IntroAction (IntroInjection _) -> Some pat.CAst.loc | _ -> None + +let decode_inj_ipat ?loc = function + (* For the "as [= pat1 ... patn ]" syntax *) + | [{ CAst.v = IntroAction (IntroInjection ipat) }] -> ipat + (* For the "as pat1 ... patn" syntax *) + | ([] | [_]) as ipat -> ipat + | pat1::pat2::_ as ipat -> + (* To be sure that there is no confusion of syntax, we check that no [= ...] occurs + in the non-singleton list of patterns *) + match isInjPat pat1 with + | Some _ -> user_err ?loc:pat2.CAst.loc (str "Unexpected pattern.") + | None -> + match List.map_filter isInjPat ipat with + | loc :: _ -> user_err ?loc (str "Unexpected injection pattern.") + | [] -> ipat + } TACTIC EXTEND injection @@ -157,16 +174,16 @@ TACTIC EXTEND einjection | [ "einjection" destruction_arg(c) ] -> { mytclWithHoles (injClause None None) true c } END TACTIC EXTEND injection_as -| [ "injection" "as" intropattern_list(ipat)] -> - { injClause None (Some ipat) false None } -| [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] -> - { mytclWithHoles (injClause None (Some ipat)) false c } +| [ "injection" "as" simple_intropattern_list(ipat)] -> + { injClause None (Some (decode_inj_ipat ipat)) false None } +| [ "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)] -> - { injClause None (Some ipat) true None } -| [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] -> - { mytclWithHoles (injClause None (Some ipat)) true c } +| [ "einjection" "as" simple_intropattern_list(ipat)] -> + { injClause None (Some (decode_inj_ipat ipat)) true None } +| [ "einjection" destruction_arg(c) "as" simple_intropattern_list(ipat)] -> + { mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) true c } END TACTIC EXTEND simple_injection | [ "simple" "injection" ] -> { simpleInjClause None false None } @@ -319,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) } @@ -405,7 +422,7 @@ END open Inv open Leminv -let seff id = VtSideff [id], VtLater +let seff id = VtSideff ([id], VtLater) } @@ -914,10 +931,10 @@ END (* spiwack: I put it in extratactics because it is somewhat tied with the semantics of the LCF-style tactics, hence with the classic tactic mode. *) -VERNAC COMMAND EXTEND GrabEvars -| ![ proof ] [ "Grab" "Existential" "Variables" ] +VERNAC COMMAND EXTEND GrabEvars STATE proof +| [ "Grab" "Existential" "Variables" ] => { classify_as_proofstep } - -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p)) pstate } + -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.V82.grab_evars p) pstate } END (* Shelves all the goals under focus. *) @@ -946,10 +963,10 @@ TACTIC EXTEND unshelve END (* Command to add every unshelved variables to the focus *) -VERNAC COMMAND EXTEND Unshelve -| ![ proof ] [ "Unshelve" ] +VERNAC COMMAND EXTEND Unshelve STATE proof +| [ "Unshelve" ] => { classify_as_proofstep } - -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p)) pstate } + -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.unshelve p) pstate } END (* Gives up on the goals under focus: the goals are considered solved, @@ -1101,7 +1118,7 @@ END VERNAC COMMAND EXTEND OptimizeProof | ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } -> - { fun ~pstate -> Option.map Proof_global.compact_the_proof pstate } + { fun ~pstate -> Proof_global.compact_the_proof pstate } | [ "Optimize" "Heap" ] => { classify_as_proofstep } -> { Gc.compact () } END 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 7eb34158e8..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 @@ -376,7 +376,7 @@ let () = declare_int_option { let vernac_solve ~pstate n info tcom b = let open Goal_select in - let pstate, status = Proof_global.with_current_proof (fun etac p -> + let pstate, status = Proof_global.map_fold_proof_endline (fun etac p -> let with_end_tac = if b then Some etac else None in let global = match n with SelectAll | SelectList _ -> true | _ -> false in let info = Option.append info !print_info_trace in @@ -388,7 +388,7 @@ let vernac_solve ~pstate n info tcom b = let p = Proof.maximal_unfocus Vernacentries.command_focus p in p,status) pstate in if not status then Feedback.feedback Feedback.AddedAxiom; - Some pstate + pstate let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s @@ -434,23 +434,22 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false } -VERNAC { tactic_mode } EXTEND VernacSolve -| ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +VERNAC { tactic_mode } EXTEND VernacSolve STATE proof +| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => { classify_as_proofstep } -> { let g = Option.default (Goal_select.get_default_goal_selector ()) g in - Vernacentries.vernac_require_open_proof vernac_solve g n t def + vernac_solve g n t def } -| ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => { let anon_abstracting_tac = is_anonymous_abstract t in 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 - Vernacentries.vernac_require_open_proof vernac_solve Goal_select.SelectAll n t def + vernac_solve Goal_select.SelectAll n t def } END @@ -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 de3a9c9fa9..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 *) @@ -80,25 +80,25 @@ GRAMMAR EXTEND Gram open Obligations -let obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.obligation ~ontop:pstate obl t) tac) -let next_obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.next_obligation ~ontop:pstate obl t) tac) +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,[])) } -VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } -| ![ proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> +VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE open_proof +| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> { obligation (num, Some name, Some t) tac } -| ![ proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> +| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> { obligation (num, Some name, None) tac } -| ![ proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> +| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> { obligation (num, None, Some t) tac } -| ![ proof ] [ "Obligation" integer(num) withtac(tac) ] -> +| [ "Obligation" integer(num) withtac(tac) ] -> { obligation (num, None, None) tac } -| ![ proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> +| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> { next_obligation (Some name) tac } -| ![ proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } +| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } END VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 12b12bc7b0..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 *) @@ -180,34 +180,34 @@ TACTIC EXTEND setoid_rewrite END VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "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 atts a aeq n (Some lemma1) (Some lemma2) None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "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 atts a aeq n (Some lemma1) None None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> + | #[ 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 - | #[ atts = rewrite_attributes; ] ![ proof ] [ "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 atts a aeq n None (Some lemma2) None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + | #[ 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 - | #[ atts = rewrite_attributes; ] ![ proof ] [ "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 atts a aeq n (Some lemma1) None (Some lemma3) } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "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) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n None None (Some lemma3) } END @@ -234,65 +234,63 @@ GRAMMAR EXTEND Gram END VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "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 atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "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) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) None None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> + | #[ 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 - | #[ atts = rewrite_attributes; ] ![ proof ] [ "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 atts ~binders:b a aeq n None (Some lemma2) None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + | #[ 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 - | #[ atts = rewrite_attributes; ] ![ proof ] [ "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 atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "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) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None None (Some lemma3) } END VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> { add_setoid atts [] a aeq t n } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(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 } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] - (* This command may or may not open a goal *) - => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater } - -> { - add_morphism_infer atts m n - } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => { VtStartProof(GuaranteesOpacity,[n]), VtLater } - -> { - add_morphism atts [] m s n - } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) + | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] + => { 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) } + -> { 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]) } + -> { 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 } - -> { - add_morphism atts binders m s n - } + => { VtStartProof(GuaranteesOpacity,[n]) } + -> { add_morphism atts binders m s n } END TACTIC EXTEND setoid_symmetry @@ -310,12 +308,6 @@ TACTIC EXTEND setoid_transitivity END VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY -| ![ proof ] [ "Print" "Rewrite" "HintDb" preident(s) ] -> - { (* This command should not use the proof env, keeping previous - behavior as requested in review. *) - fun ~pstate -> - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in - Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s); - pstate } +| [ "Print" "Rewrite" "HintDb" preident(s) ] -> + { Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) } 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 963b7189f9..f977ba34d2 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 *) @@ -23,14 +23,12 @@ open Tacticals.New open Tactics open Pretype_errors open Typeclasses -open Classes open Constrexpr open Globnames open Evd open Tactypes open Locus open Locusops -open Decl_kinds open Elimschemes open Environ open Termops @@ -44,13 +42,13 @@ module NamedDecl = Context.Named.Declaration (** Typeclass-based generalized rewriting. *) -type rewrite_attributes = { polymorphic : bool; program : bool; global : bool } +type rewrite_attributes = { polymorphic : 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 } + Attributes.Notations.return { polymorphic; global } (** Constants used by the tactic. *) @@ -207,7 +205,7 @@ end) = struct let mk_relation env evd a = app_poly env evd relation [| a |] - (** Build an infered signature from constraints on the arguments and expected output + (** Build an inferred signature from constraints on the arguments and expected output relation *) let build_signature evars env m (cstrs : (types * types option) option list) @@ -948,9 +946,9 @@ let fold_match ?(force=false) env sigma c = if dep then case_dep_scheme_kind_from_prop else case_scheme_kind_from_prop else ( - if dep - then case_dep_scheme_kind_from_type_in_prop - else case_scheme_kind_from_type) + if dep + then case_dep_scheme_kind_from_type_in_prop + else case_scheme_kind_from_type) else ((* sortc <> InProp by typing *) if dep then case_dep_scheme_kind_from_type @@ -1791,20 +1789,21 @@ let rec strategy_of_ast = function let mkappc s l = CAst.make @@ CAppExpl ((None,qualid_of_ident (Id.of_string s),None),l) let declare_an_instance n s args = - (((CAst.make @@ Name n),None), Explicit, + (((CAst.make @@ Name n),None), CAst.make @@ CAppExpl ((None, qualid_of_string s,None), args)) let declare_instance a aeq n s = declare_an_instance n s [a;aeq] -let anew_instance ~pstate atts binders instance fields = - let program_mode = atts.program in - new_instance ~pstate ~program_mode atts.polymorphic - binders instance (Some (true, CAst.make @@ CRecord (fields))) - ~global:atts.global ~generalize:false Hints.empty_hint_info +let anew_instance atts binders (name,t) fields = + let _id = Classes.new_instance atts.polymorphic + name binders t (true, CAst.make @@ CRecord (fields)) + ~global:atts.global ~generalize:false Hints.empty_hint_info + in + () -let declare_instance_refl ~pstate atts 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 ~pstate atts binders instance + in anew_instance atts binders instance [(qualid_of_ident (Id.of_string "reflexivity"),lemma)] let declare_instance_sym atts binders a aeq n lemma = @@ -1817,44 +1816,44 @@ let declare_instance_trans atts binders a aeq n lemma = in anew_instance atts binders instance [(qualid_of_ident (Id.of_string "transitivity"),lemma)] -let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans = +let declare_relation atts ?(binders=[]) a aeq n refl symm trans = init_setoid (); let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in - let _, pstate = anew_instance ~pstate atts binders instance [] in + let () = anew_instance atts binders instance [] in match (refl,symm,trans) with - (None, None, None) -> pstate - | (Some lemma1, None, None) -> - snd @@ declare_instance_refl ~pstate atts binders a aeq n lemma1 - | (None, Some lemma2, None) -> - snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2 - | (None, None, Some lemma3) -> - snd @@ declare_instance_trans ~pstate atts binders a aeq n lemma3 - | (Some lemma1, Some lemma2, None) -> - let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in - snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2 - | (Some lemma1, None, Some lemma3) -> - let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in - let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in - snd @@ anew_instance ~pstate 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, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in - let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in - snd @@ anew_instance ~pstate 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, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in - let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in - let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in - snd @@ anew_instance ~pstate 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)] + (None, None, None) -> () + | (Some lemma1, None, None) -> + declare_instance_refl atts binders a aeq n lemma1 + | (None, Some lemma2, None) -> + declare_instance_sym atts binders a aeq n lemma2 + | (None, None, Some lemma3) -> + declare_instance_trans atts binders a aeq n lemma3 + | (Some lemma1, Some lemma2, None) -> + let () = declare_instance_refl atts binders a aeq n lemma1 in + declare_instance_sym atts binders a aeq n lemma2 + | (Some lemma1, None, Some lemma3) -> + let () = declare_instance_refl atts binders a aeq n lemma1 in + let () = declare_instance_trans atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in + 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 () = declare_instance_sym atts binders a aeq n lemma2 in + let () = declare_instance_trans atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in + 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 () = declare_instance_refl atts binders a aeq n lemma1 in + let () = declare_instance_sym atts binders a aeq n lemma2 in + let () = declare_instance_trans atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in + 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)] let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) @@ -1903,7 +1902,7 @@ let declare_projection n instance_id r = Declare.definition_entry ~types:typ ~univs term in ignore(Declare.declare_constant n - (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) + (Declare.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) let build_morphism_signature env sigma m = let m,ctx = Constrintern.interp_constr env sigma m in @@ -1950,19 +1949,18 @@ 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 ~pstate atts 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, pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in - let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in - let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in + let () = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in + let () = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in + let () = 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 - snd @@ anew_instance ~pstate 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])] - + 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])] let make_tactic name = let open Tacexpr in @@ -1973,58 +1971,63 @@ 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 ~pstate atts m n : Proof_global.t option = +let add_morphism_as_parameter atts m n : unit = + init_setoid (); + 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 + let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id + (Declare.ParameterEntry + (None,(instance,uctx),None), + Decl_kinds.IsAssumption Decl_kinds.Logical) + in + Classes.add_instance (Classes.mk_instance + (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); + declare_projection n instance_id (ConstRef cst) + +let add_morphism_interactive atts m n : Lemmas.t = warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); - (* 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.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 (Classes.mk_instance - (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); - declare_projection n instance_id (ConstRef cst); - pstate - else - 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 - let hook _ _ _ = function - | Globnames.ConstRef cst -> - add_instance (Classes.mk_instance - (PropGlobal.proper_class env evd) Hints.empty_hint_info - atts.global (ConstRef cst)); - declare_projection n instance_id (ConstRef cst) - | _ -> assert false - in - let hook = Lemmas.mk_hook hook in - Flags.silently - (fun () -> - let pstate = Lemmas.start_proof ~ontop:pstate ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in - Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) () + let kind = Decl_kinds.Global Decl_kinds.ImportDefaultBehavior, atts.polymorphic, + Decl_kinds.DefinitionBody Decl_kinds.Instance + in + let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in + let hook _ _ _ = function + | Globnames.ConstRef cst -> + Classes.add_instance (Classes.mk_instance + (PropGlobal.proper_class env evd) Hints.empty_hint_info + atts.global (ConstRef cst)); + declare_projection n instance_id (ConstRef cst) + | _ -> assert false + in + let hook = DeclareDef.Hook.make hook in + Flags.silently + (fun () -> + let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in + fst (Lemmas.by (Tacinterp.interp tac) lemma)) () -let add_morphism ~pstate atts binders m s n = +let add_morphism atts binders m s n = init_setoid (); let instance_id = add_suffix n "_Proper" in - let instance = - (((CAst.make @@ Name instance_id),None), Explicit, - CAst.make @@ CAppExpl ( - (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), - [cHole; s; m])) + let instance_name = (CAst.make @@ Name instance_id),None in + let instance_t = + CAst.make @@ CAppExpl + ((None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), + [cHole; s; m]) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - let _, pstate = new_instance ~pstate ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance - None - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in - pstate + let _id, lemma = Classes.new_instance_interactive + ~global:atts.global atts.polymorphic + instance_name binders instance_t + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info + in + lemma (* no instance body -> always open proof *) (** Bind to "rewrite" too *) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index a200cb5ced..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 *) @@ -81,18 +81,36 @@ val cl_rewrite_clause : val is_applied_rewrite_relation : env -> evar_map -> rel_context -> constr -> types option -val declare_relation : pstate:Proof_global.t option -> rewrite_attributes -> - ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> - constr_expr option -> constr_expr option -> constr_expr option -> Proof_global.t option - -val add_setoid : pstate:Proof_global.t option -> - rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr -> - Id.t -> Proof_global.t option - -val add_morphism_infer : pstate:Proof_global.t option -> rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option - -val add_morphism : pstate:Proof_global.t option -> - rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option +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 + : rewrite_attributes + -> local_binder_expr list + -> constr_expr + -> constr_expr + -> constr_expr + -> Id.t + -> unit + +val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Lemmas.t +val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit + +val add_morphism + : rewrite_attributes + -> local_binder_expr list + -> constr_expr + -> constr_expr + -> Id.t + -> Lemmas.t val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr 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 0eb7726a18..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 *) @@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) | Select (* returns all successes of the first matching branch *) - | Once (* returns the first success in a maching branch + | Once (* returns the first success in a matching branch (not necessarily the first) *) type global_flag = (* [gfail] or [fail] *) | TacGlobal diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index fd303f5d94..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 *) @@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) | Select (* returns all successes of the first matching branch *) - | Once (* returns the first success in a maching branch + | Once (* returns the first success in a matching branch (not necessarily the first) *) type global_flag = (* [gfail] or [fail] *) | TacGlobal 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 800be2565d..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 *) @@ -855,7 +855,7 @@ let interp_binding_name ist env sigma = function | NamedHyp id -> (* If a name is bound, it has to be a quantified hypothesis *) (* user has to use other names for variables if these ones clash with *) - (* a name intented to be used as a (non-variable) identifier *) + (* a name intended to be used as a (non-variable) identifier *) try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (make id) with Not_found -> NamedHyp id @@ -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); @@ -2075,7 +2076,7 @@ let _ = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun; poly; extra; } in let tac = interp_tactic ist tac in - (* EJGA: We sould also pass the proof name if desired, for now + (* EJGA: We should also pass the proof name if desired, for now poly seems like enough to get reasonable behavior in practice *) let name, poly = Id.of_string "ltac_gen", poly in 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 2b5e496168..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 *) @@ -128,7 +128,7 @@ module PatternMatching (E:StaticEnvironment) = struct (** To focus on the algorithmic portion of pattern-matching, the bookkeeping is relegated to a monad: the composition of the - bactracking monad of {!IStream.t} with a "writer" effect. *) + backtracking monad of {!IStream.t} with a "writer" effect. *) (* spiwack: as we don't benefit from the various stream optimisations of Haskell, it may be costly to give the monad in direct style such as here. We may want to use some continuation passing style. *) 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 *) |