aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/ltac/tacinterp.ml24
-rw-r--r--plugins/micromega/EnvRing.v2
-rw-r--r--plugins/micromega/RingMicromega.v2
-rw-r--r--plugins/micromega/Tauto.v1
-rw-r--r--plugins/micromega/VarMap.v1
-rw-r--r--plugins/rtauto/Bintree.v4
-rw-r--r--plugins/setoid_ring/Field_theory.v3
-rw-r--r--plugins/setoid_ring/InitialRing.v1
-rw-r--r--plugins/setoid_ring/Ncring_polynom.v2
-rw-r--r--plugins/setoid_ring/Ring_polynom.v2
-rw-r--r--plugins/setoid_ring/Ring_theory.v1
-rw-r--r--plugins/ssr/ssrast.mli5
-rw-r--r--plugins/ssr/ssrbool.v11
-rw-r--r--plugins/ssr/ssreflect.v5
-rw-r--r--plugins/ssr/ssrfun.v2
-rw-r--r--plugins/ssr/ssrfwd.ml4
-rw-r--r--plugins/ssr/ssripats.ml16
-rw-r--r--plugins/ssr/ssrparser.mlg22
-rw-r--r--plugins/ssr/ssrprinters.ml4
20 files changed, 75 insertions, 39 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 98aaa081c3..4b6caea70d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1494,7 +1494,7 @@ let do_build_inductive
let _time2 = System.get_time () in
try
with_full_print
- (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds false false false ~uniform:ComInductive.NonUniformParameters))
+ (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false false false ~uniform:ComInductive.NonUniformParameters))
Declarations.Finite
with
| UserError(s,msg) as e ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 816741b894..3e7479903a 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -104,7 +104,7 @@ let pr_appl h vs =
let rec name_with_list appl t =
match appl with
| [] -> t
- | (h,vs)::l -> Proofview.Trace.name_tactic (fun () -> pr_appl h vs) (name_with_list l t)
+ | (h,vs)::l -> Proofview.Trace.name_tactic (fun _ _ -> pr_appl h vs) (name_with_list l t)
let name_if_glob appl t =
match appl with
| UnnamedAppl -> t
@@ -1050,7 +1050,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
return (hov 0 msg , hov 0 msg)
in
let print (_,msgnl) = Proofview.(tclLIFT (NonLogical.print_info msgnl)) in
- let log (msg,_) = Proofview.Trace.log (fun () -> msg) in
+ let log (msg,_) = Proofview.Trace.log (fun _ _ -> msg) in
let break = Proofview.tclLIFT (db_breakpoint (curr_debug ist) s) in
Ftactic.run msgnl begin fun msgnl ->
print msgnl <*> log msgnl <*> break
@@ -1132,7 +1132,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
in
let tac =
Ftactic.with_env interp_vars >>= fun (env, lr) ->
- let name () = Pptactic.pr_alias (fun v -> print_top_val env v) 0 s lr in
+ let name _ _ = Pptactic.pr_alias (fun v -> print_top_val env v) 0 s lr in
Proofview.Trace.name_tactic name (tac lr)
(* spiwack: this use of name_tactic is not robust to a
change of implementation of [Ftactic]. In such a situation,
@@ -1153,7 +1153,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let tac = Tacenv.interp_ml_tactic opn in
let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
let tac args =
- let name () = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in
+ let name _ _ = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in
Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist))
in
Ftactic.run args tac
@@ -1539,7 +1539,7 @@ and name_atomic ?env tacexpr tac : unit Proofview.tactic =
| None -> Proofview.tclENV
end >>= fun env ->
Proofview.tclEVARMAP >>= fun sigma ->
- let name () = Pptactic.pr_atomic_tactic env sigma tacexpr in
+ let name _ _ = Pptactic.pr_atomic_tactic env sigma tacexpr in
Proofview.Trace.name_tactic name tac
(* Interprets a primitive tactic *)
@@ -1560,7 +1560,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end
| TacApply (a,ev,cb,cl) ->
(* spiwack: until the tactic is in the monad *)
- Proofview.Trace.name_tactic (fun () -> Pp.str"<apply>") begin
+ Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<apply>") begin
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
@@ -1601,7 +1601,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end
| TacMutualFix (id,n,l) ->
(* spiwack: until the tactic is in the monad *)
- Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin
+ Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<mutual fix>") begin
Proofview.Goal.enter begin fun gl ->
let env = pf_env gl in
let f sigma (id,n,c) =
@@ -1616,7 +1616,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end
| TacMutualCofix (id,l) ->
(* spiwack: until the tactic is in the monad *)
- Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin
+ Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<mutual cofix>") begin
Proofview.Goal.enter begin fun gl ->
let env = pf_env gl in
let f sigma (id,c) =
@@ -1731,7 +1731,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end
| TacChange (None,c,cl) ->
(* spiwack: until the tactic is in the monad *)
- Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
+ Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<change>") begin
Proofview.Goal.enter begin fun gl ->
let is_onhyps = match cl.onhyps with
| None | Some [] -> true
@@ -1756,7 +1756,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end
| TacChange (Some op,c,cl) ->
(* spiwack: until the tactic is in the monad *)
- Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
+ Proofview.Trace.name_tactic (fun _ _ -> Pp.str"<change>") begin
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
@@ -1957,7 +1957,9 @@ let lifts f = (); fun ist x -> Ftactic.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let (sigma, v) = f ist env sigma x in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (Ftactic.return v)
+ (* FIXME once we don't need to catch side effects *)
+ (Proofview.tclTHEN (Proofview.Unsafe.tclSETENV (Global.env()))
+ (Ftactic.return v))
end
let interp_bindings' ist bl = Ftactic.return begin fun env sigma ->
diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 4042959b50..eb84b1203d 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -118,6 +118,7 @@ Section MakeRingPol.
- (Pinj i (Pc c)) is (Pc c)
*)
+ #[universes(template)]
Inductive Pol : Type :=
| Pc : C -> Pol
| Pinj : positive -> Pol -> Pol
@@ -939,6 +940,7 @@ Qed.
(** Definition of polynomial expressions *)
+ #[universes(template)]
Inductive PExpr : Type :=
| PEc : C -> PExpr
| PEX : positive -> PExpr
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index f066ea462f..782fab5e68 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -289,6 +289,7 @@ destruct o' ; rewrite H1 ; now rewrite (Rplus_0_l sor).
now apply (Rplus_nonneg_nonneg sor).
Qed.
+#[universes(template)]
Inductive Psatz : Type :=
| PsatzIn : nat -> Psatz
| PsatzSquare : PolC -> Psatz
@@ -685,6 +686,7 @@ end.
Definition eval_pexpr : PolEnv -> PExpr C -> R :=
PEeval rplus rtimes rminus ropp phi pow_phi rpow.
+#[universes(template)]
Record Formula (T:Type) : Type := {
Flhs : PExpr T;
Fop : Op2;
diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index 458844e1b9..587f2f1fa4 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -21,6 +21,7 @@ Require Import Bool.
Set Implicit Arguments.
+ #[universes(template)]
Inductive BFormula (A:Type) : Type :=
| TT : BFormula A
| FF : BFormula A
diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index 2d2c0bc77a..c888f9af45 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -30,6 +30,7 @@ Section MakeVarMap.
Variable A : Type.
Variable default : A.
+ #[universes(template)]
Inductive t : Type :=
| Empty : t
| Leaf : A -> t
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 99c02995fb..751f0d8334 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -81,10 +81,12 @@ Section Store.
Variable A:Type.
+#[universes(template)]
Inductive Poption : Type:=
PSome : A -> Poption
| PNone : Poption.
+#[universes(template)]
Inductive Tree : Type :=
Tempty : Tree
| Branch0 : Tree -> Tree -> Tree
@@ -177,6 +179,7 @@ generalize i;clear i;induction j;destruct T;simpl in H|-*;
destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence.
Qed.
+#[universes(template)]
Record Store : Type :=
mkStore {index:positive;contents:Tree}.
@@ -191,6 +194,7 @@ Lemma get_empty : forall i, get i empty = PNone.
intro i; case i; unfold empty,get; simpl;reflexivity.
Qed.
+#[universes(template)]
Inductive Full : Store -> Type:=
F_empty : Full empty
| F_push : forall a S, Full S -> Full (push a S).
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index ce115f564f..dba72337b2 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -730,6 +730,7 @@ Qed.
(* The input: syntax of a field expression *)
+#[universes(template)]
Inductive FExpr : Type :=
| FEO : FExpr
| FEI : FExpr
@@ -762,6 +763,7 @@ Strategy expand [FEeval].
(* The result of the normalisation *)
+#[universes(template)]
Record linear : Type := mk_linear {
num : PExpr C;
denum : PExpr C;
@@ -944,6 +946,7 @@ induction e2; intros p1 p2;
now rewrite <- PEpow_mul_r.
Qed.
+#[universes(template)]
Record rsplit : Type := mk_rsplit {
rsplit_left : PExpr C;
rsplit_common : PExpr C;
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index f5db275465..15d490a6ab 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -740,6 +740,7 @@ Ltac abstract_ring_morphism set ext rspec :=
| _ => fail 1 "bad ring structure"
end.
+#[universes(template)]
Record hypo : Type := mkhypo {
hypo_type : Type;
hypo_proof : hypo_type
diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v
index 12208ff6b9..31182f51e2 100644
--- a/plugins/setoid_ring/Ncring_polynom.v
+++ b/plugins/setoid_ring/Ncring_polynom.v
@@ -32,6 +32,7 @@ Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x.
with coefficients in C :
*)
+#[universes(template)]
Inductive Pol : Type :=
| Pc : C -> Pol
| PX : Pol -> positive -> positive -> Pol -> Pol.
@@ -43,6 +44,7 @@ Definition cI:C . exact ring1. Defined.
Definition P1 := Pc 1.
Variable Ceqb:C->C->bool.
+#[universes(template)]
Class Equalityb (A : Type):= {equalityb : A -> A -> bool}.
Notation "x =? y" := (equalityb x y) (at level 70, no associativity).
Variable Ceqb_eq: forall x y:C, Ceqb x y = true -> (x == y).
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index ccd82eabcd..9ef24144d2 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -121,6 +121,7 @@ Section MakeRingPol.
- (Pinj i (Pc c)) is (Pc c)
*)
+ #[universes(template)]
Inductive Pol : Type :=
| Pc : C -> Pol
| Pinj : positive -> Pol -> Pol
@@ -908,6 +909,7 @@ Section MakeRingPol.
(** Definition of polynomial expressions *)
+ #[universes(template)]
Inductive PExpr : Type :=
| PEO : PExpr
| PEI : PExpr
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index d67a8d8dce..6c782269ab 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -540,6 +540,7 @@ Section AddRing.
Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
Variable req : R -> R -> Prop. *)
+#[universes(template)]
Inductive ring_kind : Type :=
| Abstract
| Computational
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index fac524da6b..dd2c2d0ba4 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -64,8 +64,6 @@ type ast_closure_term = {
type ssrview = ast_closure_term list
-type id_mod = Dependent
-
type id_block = Prefix of Id.t | SuffixId of Id.t | SuffixNum of int
(* Only [One] forces an introduction, possibly reducing the goal. *)
@@ -77,7 +75,7 @@ type anon_iter =
type ssripat =
| IPatNoop
- | IPatId of id_mod option * Id.t
+ | IPatId of Id.t
| IPatAnon of anon_iter (* inaccessible name *)
(* TODO | IPatClearMark *)
| IPatDispatch of bool (* ssr exception: accept a dispatch on the empty list even when there are subgoals *) * ssripatss_or_block (* (..|..) *)
@@ -88,6 +86,7 @@ type ssripat =
| IPatClear of ssrclear (* {H1 H2} *)
| IPatSimpl of ssrsimpl
| IPatAbstractVars of Id.t list
+ | IPatFastNondep
| IPatEqGen of unit Proofview.tactic (* internal use: generation of eqn *)
and ssripats = ssripat list
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index 3a7cf41d43..ed4ff2aa66 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -609,6 +609,7 @@ Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3.
(** Allow the direct application of a reflection lemma to a boolean assertion. **)
Coercion elimT : reflect >-> Funclass.
+#[universes(template)]
Variant implies P Q := Implies of P -> Q.
Lemma impliesP P Q : implies P Q -> P -> Q. Proof. by case. Qed.
Lemma impliesPn (P Q : Prop) : implies P Q -> ~ Q -> ~ P.
@@ -1130,10 +1131,12 @@ Proof. by move=> *; apply/orP; left. Qed.
Lemma subrelUr r1 r2 : subrel r2 (relU r1 r2).
Proof. by move=> *; apply/orP; right. Qed.
+#[universes(template)]
Variant mem_pred := Mem of pred T.
Definition isMem pT topred mem := mem = (fun p : pT => Mem [eta topred p]).
+#[universes(template)]
Structure predType := PredType {
pred_sort :> Type;
topred : pred_sort -> pred T;
@@ -1275,6 +1278,7 @@ Implicit Types (x : T) (p : pred T) (sp : simpl_pred T) (pp : pT).
implementation of unification, notably improper expansion of telescope
projections and overwriting of a variable assignment by a later
unification (probably due to conversion cache cross-talk). **)
+#[universes(template)]
Structure manifest_applicative_pred p := ManifestApplicativePred {
manifest_applicative_pred_value :> pred T;
_ : manifest_applicative_pred_value = p
@@ -1283,18 +1287,21 @@ Definition ApplicativePred p := ManifestApplicativePred (erefl p).
Canonical applicative_pred_applicative sp :=
ApplicativePred (applicative_pred_of_simpl sp).
+#[universes(template)]
Structure manifest_simpl_pred p := ManifestSimplPred {
manifest_simpl_pred_value :> simpl_pred T;
_ : manifest_simpl_pred_value = SimplPred p
}.
Canonical expose_simpl_pred p := ManifestSimplPred (erefl (SimplPred p)).
+#[universes(template)]
Structure manifest_mem_pred p := ManifestMemPred {
manifest_mem_pred_value :> mem_pred T;
_ : manifest_mem_pred_value= Mem [eta p]
}.
Canonical expose_mem_pred p := @ManifestMemPred p _ (erefl _).
+#[universes(template)]
Structure applicative_mem_pred p :=
ApplicativeMemPred {applicative_mem_pred_value :> manifest_mem_pred p}.
Canonical check_applicative_mem_pred p (ap : manifest_applicative_pred p) mp :=
@@ -1345,6 +1352,7 @@ End simpl_mem.
(** Qualifiers and keyed predicates. **)
+#[universes(template)]
Variant qualifier (q : nat) T := Qualifier of predPredType T.
Coercion has_quality n T (q : qualifier n T) : pred_class :=
@@ -1392,9 +1400,11 @@ Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T => P%B))
Section KeyPred.
Variable T : Type.
+#[universes(template)]
Variant pred_key (p : predPredType T) := DefaultPredKey.
Variable p : predPredType T.
+#[universes(template)]
Structure keyed_pred (k : pred_key p) :=
PackKeyedPred {unkey_pred :> pred_class; _ : unkey_pred =i p}.
@@ -1426,6 +1436,7 @@ Section KeyedQualifier.
Variables (T : Type) (n : nat) (q : qualifier n T).
+#[universes(template)]
Structure keyed_qualifier (k : pred_key q) :=
PackKeyedQualifier {unkey_qualifier; _ : unkey_qualifier = q}.
Definition KeyedQualifier k := PackKeyedQualifier k (erefl q).
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 7596f6638a..4721e19a8b 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -178,6 +178,7 @@ Register abstract_key as plugins.ssreflect.abstract_key.
Register abstract as plugins.ssreflect.abstract.
(** Constants for tactic-views **)
+#[universes(template)]
Inductive external_view : Type := tactic_view of Type.
(**
@@ -206,6 +207,7 @@ Inductive external_view : Type := tactic_view of Type.
Module TheCanonical.
+#[universes(template)]
Variant put vT sT (v1 v2 : vT) (s : sT) := Put.
Definition get vT sT v s (p : @put vT sT v v s) := let: Put _ _ _ := p in s.
@@ -301,9 +303,11 @@ Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s)
We also define a simpler version ("phant" / "Phant") of phantom for the
common case where p_type is Type. **)
+#[universes(template)]
Variant phantom T (p : T) := Phantom.
Arguments phantom : clear implicits.
Arguments Phantom : clear implicits.
+#[universes(template)]
Variant phant (p : Type) := Phant.
(** Internal tagging used by the implementation of the ssreflect elim. **)
@@ -389,6 +393,7 @@ Ltac ssrdone0 :=
| match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
(** To unlock opaque constants. **)
+#[universes(template)]
Structure unlockable T v := Unlockable {unlocked : T; _ : unlocked = v}.
Lemma unlock T x C : @unlocked T x C = x. Proof. by case: C. Qed.
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index 6535cad8b7..b51ffada0c 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -285,6 +285,7 @@ Lemma unitE : all_equal_to tt. Proof. by case. Qed.
(** A generic wrapper type **)
+#[universes(template)]
Structure wrapped T := Wrap {unwrap : T}.
Canonical wrap T x := @Wrap T x.
@@ -334,6 +335,7 @@ Section SimplFun.
Variables aT rT : Type.
+#[universes(template)]
Variant simpl_fun := SimplFun of aT -> rT.
Definition fun_of_simpl f := fun x => let: SimplFun lam := f in lam x.
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 37c583ab53..257ecd2a85 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -206,7 +206,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
let mkabs gen = abs_wgen false (fun x -> x) gen in
let mkclr gen clrs = clr_of_wgen gen clrs in
let mkpats = function
- | _, Some ((x, _), _) -> fun pats -> IPatId (None,hoi_id x) :: pats
+ | _, Some ((x, _), _) -> fun pats -> IPatId (hoi_id x) :: pats
| _ -> fun x -> x in
let ct = match Ssrcommon.ssrterm_of_ast_closure_term ct with
| (a, (b, Some ct)) ->
@@ -265,7 +265,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
if gens = [] then errorstrm(str"gen have requires some generalizations");
let clear0 = old_cleartac clr0 in
let id, name_general_hyp, cleanup, pats = match id, pats with
- | None, (IPatId(_, id) as ip)::pats -> Some id, tacipat [ip], clear0, pats
+ | None, (IPatId id as ip)::pats -> Some id, tacipat [ip], clear0, pats
| None, _ -> None, Tacticals.tclIDTAC, clear0, pats
| Some (Some id),_ -> Some id, introid id, clear0, pats
| Some _,_ ->
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index e71e1bae0d..ce81d83661 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -292,7 +292,7 @@ let tac_intro_seed interp_ipats fix = Goal.enter begin fun gl ->
| Prefix fix -> Id.to_string fix ^ Id.to_string id
| SuffixNum n -> Id.to_string id ^ string_of_int n
| SuffixId fix -> Id.to_string id ^ Id.to_string fix in
- IPatId (None, Id.of_string s)) seeds in
+ IPatId (Id.of_string s)) seeds in
interp_ipats ipats
end end
@@ -377,9 +377,8 @@ let rec ipat_tac1 ipat : bool tactic =
| IPatDispatch(_,Block id_block) ->
tac_intro_seed ipat_tac id_block <*> notTAC
- | IPatId (None, id) -> Ssrcommon.tclINTRO_ID id <*> notTAC
- | IPatId (Some Dependent, id) ->
- intro_anon_deps <*> Ssrcommon.tclINTRO_ID id <*> notTAC
+ | IPatId id -> Ssrcommon.tclINTRO_ID id <*> notTAC
+ | IPatFastNondep -> intro_anon_deps <*> notTAC
| IPatCase (Block id_block) ->
Ssrcommon.tclWITHTOP tac_case <*> tac_intro_seed ipat_tac id_block <*> notTAC
@@ -456,7 +455,7 @@ let elaborate_ipats l =
| IPatDispatch(s, Regular p) :: rest -> IPatDispatch (s, Regular (List.map elab p)) :: elab rest
| IPatCase (Regular p) :: rest -> IPatCase (Regular (List.map elab p)) :: elab rest
| IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest
- | (IPatEqGen _ | IPatId _ | IPatSimpl _ | IPatClear _ |
+ | (IPatEqGen _ | IPatId _ | IPatSimpl _ | IPatClear _ | IPatFastNondep |
IPatAnon _ | IPatView _ | IPatNoop | IPatRewrite _ |
IPatAbstractVars _ | IPatDispatch(_, Block _) | IPatCase(Block _)) as x :: rest -> x :: elab rest
in
@@ -512,8 +511,7 @@ let mkCoqRefl t c env sigma =
let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr =
let intro_eq =
match eqid with
- | Some (IPatId (Some _, _)) -> assert false (* parser *)
- | Some (IPatId (None,ipat)) when not is_rec ->
+ | Some (IPatId ipat) when not is_rec ->
let rec intro_eq () = Goal.enter begin fun g ->
let sigma, env, concl = Goal.(sigma g, env g, concl g) in
match EConstr.kind_of_type sigma concl with
@@ -527,7 +525,7 @@ let elim_intro_tac ipats ?seed what eqid ssrelim is_rec clr =
|_ -> Ssrcommon.errorstrm (Pp.str "Too many names in intro pattern")
end in
intro_eq ()
- | Some (IPatId (None,ipat)) ->
+ | Some (IPatId ipat) ->
let intro_lhs = Goal.enter begin fun g ->
let sigma = Goal.sigma g in
let elim_name = match clr, what with
@@ -860,7 +858,7 @@ let ssrabstract dgens =
let ipats = List.map (fun (_,cp) ->
match id_of_pattern (interp_cpattern gl0 cp None) with
| None -> IPatAnon (One None)
- | Some id -> IPatId (None,id))
+ | Some id -> IPatId id)
(List.tl gens) in
conclusion ipats
end in
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 6938bbc9f6..76726009ac 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -605,7 +605,7 @@ let remove_loc x = x.CAst.v
let ipat_of_intro_pattern p = Tactypes.(
let rec ipat_of_intro_pattern = function
- | IntroNaming (IntroIdentifier id) -> IPatId (None,id)
+ | IntroNaming (IntroIdentifier id) -> IPatId id
| IntroAction IntroWildcard -> IPatAnon Drop
| IntroAction (IntroOrAndPattern (IntroOrPattern iorpat)) ->
IPatCase (Regular(
@@ -629,8 +629,8 @@ let ipat_of_intro_pattern p = Tactypes.(
)
let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function
- | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x
- | IPatId (m,id) -> IPatId (m,map_id id)
+ | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop | IPatFastNondep) as x -> x
+ | IPatId id -> IPatId (map_id id)
| IPatAbstractVars l -> IPatAbstractVars (List.map map_id l)
| IPatClear clr -> IPatClear (List.map map_ssrhyp clr)
| IPatCase (Regular iorpat) -> IPatCase (Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat))
@@ -707,7 +707,7 @@ let interp_ipat ist gl =
end
| x -> x in
let rec interp = function
- | IPatId(_, id) when ltacvar id ->
+ | IPatId id when ltacvar id ->
ipat_of_intro_pattern (interp_introid ist gl id)
| IPatId _ as x -> x
| IPatClear clr ->
@@ -729,7 +729,7 @@ let interp_ipat ist gl =
IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l))
| IPatView (clr,l) -> IPatView (clr,List.map (fun x -> snd(interp_ast_closure_term ist
gl x)) l)
- | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop) as x -> x
+ | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop | IPatFastNondep) as x -> x
| IPatEqGen _ -> assert false (*internal usage only *)
in
interp
@@ -751,8 +751,8 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats }
GLOBALIZED BY { intern_ipats }
| [ "_" ] -> { [IPatAnon Drop] }
| [ "*" ] -> { [IPatAnon All] }
- | [ ">" ident(id) ] -> { [IPatId(Some Dependent,id)] }
- | [ ident(id) ] -> { [IPatId (None,id)] }
+ | [ ">" ] -> { [IPatFastNondep] }
+ | [ ident(id) ] -> { [IPatId id] }
| [ "?" ] -> { [IPatAnon (One None)] }
| [ "+" ] -> { [IPatAnon Temporary] }
| [ "++" ] -> { [IPatAnon Temporary; IPatAnon Temporary] }
@@ -1492,7 +1492,7 @@ END
{
let intro_id_to_binder = List.map (function
- | IPatId (None,id) ->
+ | IPatId id ->
let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in
(FwdPose, [BFvar]),
CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)],
@@ -1502,8 +1502,8 @@ let intro_id_to_binder = List.map (function
let binder_to_intro_id = CAst.(List.map (function
| (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) }
| (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } ->
- List.map (function {v=Name id} -> IPatId (None,id) | _ -> IPatAnon (One None)) ids
- | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId (None,id)]
+ List.map (function {v=Name id} -> IPatId id | _ -> IPatAnon (One None)) ids
+ | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId id]
| (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon (One None)]
| _ -> anomaly "ssrbinder is not a binder"))
@@ -1994,7 +1994,7 @@ let test_ssreqid = Pcoq.Entry.of_parser "test_ssreqid" accept_ssreqid
GRAMMAR EXTEND Gram
GLOBAL: ssreqid;
ssreqpat: [
- [ id = Prim.ident -> { IPatId (None,id) }
+ [ id = Prim.ident -> { IPatId id }
| "_" -> { IPatAnon Drop }
| "?" -> { IPatAnon (One None) }
| "+" -> { IPatAnon Temporary }
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 6ccefa1cab..898e03b00e 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -97,8 +97,7 @@ let pr_view2 = pr_list mt (fun c -> str "/" ++ pr_ast_closure_term c)
let rec pr_ipat p =
match p with
- | IPatId (None,id) -> Id.print id
- | IPatId (Some Dependent,id) -> str">" ++ Id.print id
+ | IPatId id -> Id.print id
| IPatSimpl sim -> pr_simpl sim
| IPatClear clr -> pr_clear mt clr
| IPatCase (Regular iorpat) -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]")
@@ -115,6 +114,7 @@ let rec pr_ipat p =
| IPatAnon Temporary -> str "+"
| IPatNoop -> str "-"
| IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]"
+ | IPatFastNondep -> str">"
| IPatEqGen _ -> str "<tac>"
and pr_ipats ipats = pr_list spc pr_ipat ipats
and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 14:06:41 +0000