aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.mlg39
-rw-r--r--plugins/ltac/g_ltac.mlg14
-rw-r--r--plugins/ltac/g_obligations.mlg18
-rw-r--r--plugins/ltac/g_rewrite.mlg72
-rw-r--r--plugins/ltac/rewrite.ml183
-rw-r--r--plugins/ltac/rewrite.mli42
-rw-r--r--plugins/ltac/tacexpr.ml2
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--plugins/ltac/tacinterp.ml4
-rw-r--r--plugins/ltac/tactic_matching.ml2
10 files changed, 204 insertions, 174 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index f5098d2a34..0ded60d9c7 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -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
@@ -158,15 +175,15 @@ TACTIC EXTEND einjection
END
TACTIC EXTEND injection_as
| [ "injection" "as" intropattern_list(ipat)] ->
- { injClause None (Some ipat) false None }
+ { injClause None (Some (decode_inj_ipat ipat)) false None }
| [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] ->
- { mytclWithHoles (injClause None (Some ipat)) false c }
+ { 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 }
+ { injClause None (Some (decode_inj_ipat ipat)) true None }
| [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] ->
- { mytclWithHoles (injClause None (Some ipat)) true c }
+ { mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) true c }
END
TACTIC EXTEND simple_injection
| [ "simple" "injection" ] -> { simpleInjClause None false None }
@@ -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.modify_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.modify_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/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 7eb34158e8..960e5b76f8 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -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.with_proof (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,13 +434,13 @@ 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
@@ -450,7 +450,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve
VtLater
} -> {
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
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index de3a9c9fa9..58c8dabd79 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -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)
}
-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..1a84158df7 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -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) ]
+ | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
+ => { VtStartProof(GuaranteesOpacity, [n]), VtLater }
+ -> { 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]), VtLater }
- -> {
- add_morphism atts [] m s n
- }
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
+ -> { 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
- }
+ -> { 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/rewrite.ml b/plugins/ltac/rewrite.ml
index 775d3969db..e0a31e7dba 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -23,7 +23,6 @@ open Tacticals.New
open Tactics
open Pretype_errors
open Typeclasses
-open Classes
open Constrexpr
open Globnames
open Evd
@@ -43,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. *)
@@ -206,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)
@@ -1795,15 +1794,16 @@ let declare_an_instance n s args =
let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
-let anew_instance ~pstate atts binders (name,t) fields =
- let program_mode = atts.program in
- new_instance ~pstate ~program_mode atts.polymorphic
- name binders t (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 =
@@ -1816,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)
@@ -1949,18 +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 =
@@ -1972,45 +1972,48 @@ 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
+ (Entries.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 : Proof_global.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, 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 = Lemmas.mk_hook hook in
+ Flags.silently
+ (fun () ->
+ let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+ fst Pfedit.(by (Tacinterp.interp tac) pstate)) ()
-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_name = (CAst.make @@ Name instance_id),None in
@@ -2020,12 +2023,12 @@ let add_morphism ~pstate atts binders m s n =
[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
- instance_name binders instance_t None
+ let _id, pstate = 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
- pstate
+ pstate (* no instance body -> always open proof *)
(** Bind to "rewrite" too *)
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index a200cb5ced..3ef33c6dc9 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -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 -> Proof_global.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
+ -> Proof_global.t
val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 0eb7726a18..8bd69dd4fd 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -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..f839c3e886 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -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/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 800be2565d..4a0b01bcdc 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -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
@@ -2075,7 +2075,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/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 2b5e496168..7783661787 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -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. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 12:38:51 +0000