aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success')
-rw-r--r--test-suite/success/AdvancedTypeClasses.v4
-rw-r--r--test-suite/success/ImplicitArguments.v2
-rw-r--r--test-suite/success/Inductive.v2
-rw-r--r--test-suite/success/Inversion.v2
-rw-r--r--test-suite/success/RecTutorial.v12
-rw-r--r--test-suite/success/Record.v2
-rw-r--r--test-suite/success/Scopes.v2
-rw-r--r--test-suite/success/ShowExtraction.v2
-rw-r--r--test-suite/success/Typeclasses.v4
-rw-r--r--test-suite/success/apply.v2
-rw-r--r--test-suite/success/cc.v14
-rw-r--r--test-suite/success/dependentind.v2
-rw-r--r--test-suite/success/evars.v2
-rw-r--r--test-suite/success/implicit.v12
-rw-r--r--test-suite/success/name_mangling.v3
-rw-r--r--test-suite/success/ssr_delayed_clear_rename.v5
16 files changed, 45 insertions, 27 deletions
diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v
index b4efa7edca..d0aa5c8578 100644
--- a/test-suite/success/AdvancedTypeClasses.v
+++ b/test-suite/success/AdvancedTypeClasses.v
@@ -28,8 +28,8 @@ Class interp_pair (abs : Type) :=
{ repr : term;
link: abs = interp repr }.
-Implicit Arguments repr [[interp_pair]].
-Implicit Arguments link [[interp_pair]].
+Arguments repr _ {interp_pair}.
+Arguments link _ {interp_pair}.
Lemma prod_interp `{interp_pair a, interp_pair b} : a * b = interp (Prod (repr a) (repr b)).
simpl. intros. rewrite <- link. rewrite <- (link b). reflexivity.
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index 921433cadd..9a19b595ef 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -2,7 +2,7 @@ Inductive vector {A : Type} : nat -> Type :=
| vnil : vector 0
| vcons : A -> forall {n'}, vector n' -> vector (S n').
-Implicit Arguments vector [].
+Arguments vector A : clear implicits.
Require Import Coq.Program.Program.
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 5b1482fd58..f07c0191f1 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -73,7 +73,7 @@ CoInductive LList (A : Set) : Set :=
| LNil : LList A
| LCons : A -> LList A -> LList A.
-Implicit Arguments LNil [A].
+Arguments LNil [A].
Inductive Finite (A : Set) : LList A -> Prop :=
| Finite_LNil : Finite LNil
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index 45c71615fc..ca8da39482 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type :=
| in_first : forall e, in_extension r (add_rule r e)
| in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e).
-Implicit Arguments NL [I].
+Arguments NL [I].
Inductive super_extension (I : Set) (e : extension I) :
extension I -> Type :=
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 8419404925..29350d620e 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -991,10 +991,10 @@ Proof.
Qed.
-Implicit Arguments Vector.cons [A n].
-Implicit Arguments Vector.nil [A].
-Implicit Arguments Vector.hd [A n].
-Implicit Arguments Vector.tl [A n].
+Arguments Vector.cons [A] _ [n].
+Arguments Vector.nil [A].
+Arguments Vector.hd [A n].
+Arguments Vector.tl [A n].
Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n.
Proof.
@@ -1064,7 +1064,7 @@ Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v}
| S n', Vector.cons _ v' => vector_nth A n' _ v'
end.
-Implicit Arguments vector_nth [A p].
+Arguments vector_nth [A] _ [p].
Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i a b,
@@ -1159,7 +1159,7 @@ infiniteproof map_iterate'.
Qed.
-Implicit Arguments LNil [A].
+Arguments LNil [A].
Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A),
LNil <> (LCons a l).
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 6f27c1d369..18ebcd6384 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -5,7 +5,7 @@ Require Import Program.
Require Import List.
Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }.
-Implicit Arguments vector [].
+Arguments vector : clear implicits.
Coercion vec_list : vector >-> list.
diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v
index ca37467166..2da630633d 100644
--- a/test-suite/success/Scopes.v
+++ b/test-suite/success/Scopes.v
@@ -11,7 +11,7 @@ Check (A.opp 3).
Record B := { f :> Z -> Z }.
Variable a:B.
-Arguments Scope a [Z_scope].
+Arguments a _%Z_scope : extra scopes.
Check a 0.
(* Check that casts activate scopes if ever possible *)
diff --git a/test-suite/success/ShowExtraction.v b/test-suite/success/ShowExtraction.v
index e34c240c5d..a4a35003df 100644
--- a/test-suite/success/ShowExtraction.v
+++ b/test-suite/success/ShowExtraction.v
@@ -12,7 +12,7 @@ Fail Show Extraction.
Lemma decListA : forall (xs ys : list A), {xs=ys}+{xs<>ys}.
Proof.
Show Extraction.
-fix 1.
+fix decListA 1.
destruct xs as [|x xs], ys as [|y ys].
Show Extraction.
- now left.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index cd6eac35cf..400479ae85 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -128,8 +128,8 @@ Record Monad {m : Type -> Type} := {
Print Visibility.
Print unit.
-Implicit Arguments unit [[m] [m0] [α]].
-Implicit Arguments Monad [].
+Arguments unit {m m0 α}.
+Arguments Monad : clear implicits.
Notation "'return' t" := (unit t).
(* Test correct handling of existentials and defined fields. *)
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 02e043bc36..b287b5facf 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -39,7 +39,7 @@ Qed.
(* Check apply/eapply distinction in presence of open terms *)
Parameter h : forall x y z : nat, x = z -> x = y.
-Implicit Arguments h [[x] [y]].
+Arguments h {x y}.
Goal 1 = 0 -> True.
intro H.
apply h in H || exact I.
diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v
index bbfe5ec420..49a8b9cf46 100644
--- a/test-suite/success/cc.v
+++ b/test-suite/success/cc.v
@@ -151,3 +151,17 @@ Section JLeivant.
congruence.
Qed.
End JLeivant.
+
+(* An example with primitive projections *)
+
+Module PrimitiveProjections.
+Set Primitive Projections.
+Record t (A:Type) := { f : A }.
+Goal forall g (a:t nat), @f nat = g -> f a = 0 -> g a = 0.
+congruence.
+Undo.
+intros.
+unfold f in H0. (* internally turn the projection to unfolded form *)
+congruence.
+Qed.
+End PrimitiveProjections.
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index f5bb884d27..55ae54ca04 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -42,7 +42,7 @@ Inductive ctx : Type :=
Bind Scope context_scope with ctx.
Delimit Scope context_scope with ctx.
-Arguments Scope snoc [context_scope].
+Arguments snoc _%context_scope.
Notation " Γ , τ " := (snoc Γ τ) (at level 25, τ at next level, left associativity) : context_scope.
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 627794832d..5b13f35d57 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -386,7 +386,7 @@ Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }.
Record tri (R:Type->Type->Type) (S:Type->Type->Type) (T:Type->Type->Type) := mkTri {
tri0 : forall a b c, R a b -> S a c -> T b c
}.
-Implicit Arguments mkTri [R S T].
+Arguments mkTri [R S T].
Definition tri_iffT : tri iffT iffT iffT :=
(mkTri
(fun X0 X1 X2 E01 E02 =>
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index a0981311b1..23853890d8 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -33,11 +33,11 @@ Definition eq1 := fun (A:Type) (x y:A) => x=y.
Definition eq2 := fun (A:Type) (x y:A) => x=y.
Definition eq3 := fun (A:Type) (x y:A) => x=y.
-Implicit Arguments op' [].
-Global Implicit Arguments op'' [].
+Arguments op' : clear implicits.
+Global Arguments op'' : clear implicits.
-Implicit Arguments eq2 [].
-Global Implicit Arguments eq3 [].
+Arguments eq2 : clear implicits.
+Global Arguments eq3 : clear implicits.
Check (op 0 0).
Check (op' nat 0 0).
@@ -89,14 +89,14 @@ Fixpoint plus n m {struct n} :=
(* Check multiple implicit arguments signatures *)
-Implicit Arguments eq_refl [[A] [x]] [[A]].
+Arguments eq_refl {A x}, {A}.
Check eq_refl : 0 = 0.
(* Check that notations preserve implicit (since 8.3) *)
Parameter p : forall A, A -> forall n, n = 0 -> True.
-Implicit Arguments p [A n].
+Arguments p [A] _ [n].
Notation Q := (p 0).
Check Q eq_refl.
diff --git a/test-suite/success/name_mangling.v b/test-suite/success/name_mangling.v
index 571dde8805..e982414206 100644
--- a/test-suite/success/name_mangling.v
+++ b/test-suite/success/name_mangling.v
@@ -122,8 +122,7 @@ Lemma a : forall n, n = 0.
Proof.
fix a 1.
Check a.
-fix 1.
-Fail Check a0.
+Fail fix a 1.
Abort.
(* Test stability of "induction" *)
diff --git a/test-suite/success/ssr_delayed_clear_rename.v b/test-suite/success/ssr_delayed_clear_rename.v
new file mode 100644
index 0000000000..951e5aff79
--- /dev/null
+++ b/test-suite/success/ssr_delayed_clear_rename.v
@@ -0,0 +1,5 @@
+Require Import ssreflect.
+Example foo (t t1 t2 : True) : True /\ True -> True -> True.
+Proof.
+move=>[{t1 t2 t} t1 t2] t.
+Abort.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 10:24:16 +0000