aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed')
-rw-r--r--test-suite/bugs/closed/1341.v2
-rw-r--r--test-suite/bugs/closed/1844.v2
-rw-r--r--test-suite/bugs/closed/1891.v2
-rw-r--r--test-suite/bugs/closed/1951.v2
-rw-r--r--test-suite/bugs/closed/1981.v2
-rw-r--r--test-suite/bugs/closed/2362.v2
-rw-r--r--test-suite/bugs/closed/2378.v6
-rw-r--r--test-suite/bugs/closed/2404.v4
-rw-r--r--test-suite/bugs/closed/2584.v2
-rw-r--r--test-suite/bugs/closed/2667.v4
-rw-r--r--test-suite/bugs/closed/2729.v4
-rw-r--r--test-suite/bugs/closed/2830.v10
-rw-r--r--test-suite/bugs/closed/3068.v2
-rw-r--r--test-suite/bugs/closed/3513.v2
-rw-r--r--test-suite/bugs/closed/3647.v6
-rw-r--r--test-suite/bugs/closed/3732.v2
-rw-r--r--test-suite/bugs/closed/4095.v2
-rw-r--r--test-suite/bugs/closed/4865.v2
18 files changed, 29 insertions, 29 deletions
diff --git a/test-suite/bugs/closed/1341.v b/test-suite/bugs/closed/1341.v
index 8c5a38859..79a0a14d7 100644
--- a/test-suite/bugs/closed/1341.v
+++ b/test-suite/bugs/closed/1341.v
@@ -8,7 +8,7 @@ Hypothesis Xst : forall A, Equivalence (Xeq A).
Variable map : forall A B, (A -> B) -> X A -> X B.
-Implicit Arguments map [A B].
+Arguments map [A B].
Goal forall A B (a b:X (B -> A)) (c:X A) (f:A -> B -> A), Xeq _ a b -> Xeq _ b (map f c) -> Xeq _ a (map f c).
intros A B a b c f Hab Hbc.
diff --git a/test-suite/bugs/closed/1844.v b/test-suite/bugs/closed/1844.v
index 17eeb3529..c41e45900 100644
--- a/test-suite/bugs/closed/1844.v
+++ b/test-suite/bugs/closed/1844.v
@@ -5,7 +5,7 @@ Definition zeq := Z.eq_dec.
Definition update (A: Set) (x: Z) (v: A) (s: Z -> A) : Z -> A :=
fun y => if zeq x y then v else s y.
-Implicit Arguments update [A].
+Arguments update [A].
Definition ident := Z.
Parameter operator: Set.
diff --git a/test-suite/bugs/closed/1891.v b/test-suite/bugs/closed/1891.v
index 685811176..5024a5bc9 100644
--- a/test-suite/bugs/closed/1891.v
+++ b/test-suite/bugs/closed/1891.v
@@ -3,7 +3,7 @@
Definition f (A: Set) (l: T A): unit := tt.
- Implicit Arguments f [A].
+ Arguments f [A].
Lemma L (x: T unit): (unit -> T unit) -> unit.
Proof.
diff --git a/test-suite/bugs/closed/1951.v b/test-suite/bugs/closed/1951.v
index 7558b0b86..e950554c4 100644
--- a/test-suite/bugs/closed/1951.v
+++ b/test-suite/bugs/closed/1951.v
@@ -42,7 +42,7 @@ match s as a return (S a) with
pair (ind2 a0) IHl) l)
end. (* some induction principle *)
-Implicit Arguments ind [S].
+Arguments ind [S].
Lemma k : a -> Type. (* some ininteresting lemma *)
intro;pattern H;apply ind;intros.
diff --git a/test-suite/bugs/closed/1981.v b/test-suite/bugs/closed/1981.v
index 99952682d..a3d942930 100644
--- a/test-suite/bugs/closed/1981.v
+++ b/test-suite/bugs/closed/1981.v
@@ -1,4 +1,4 @@
-Implicit Arguments ex_intro [A].
+Arguments ex_intro [A].
Goal exists n : nat, True.
eapply ex_intro. exact 0. exact I.
diff --git a/test-suite/bugs/closed/2362.v b/test-suite/bugs/closed/2362.v
index febb9c7bb..10e86cd12 100644
--- a/test-suite/bugs/closed/2362.v
+++ b/test-suite/bugs/closed/2362.v
@@ -8,7 +8,7 @@ Class Pointed (M:Type -> Type) :=
Unset Implicit Arguments.
Inductive FPair (A B:Type) (neutral: B) : Type:=
fpair : forall (a:A) (b:B), FPair A B neutral.
-Implicit Arguments fpair [[A] [B] [neutral]].
+Arguments fpair {A B neutral}.
Set Implicit Arguments.
diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v
index 23a58501f..6d73d58d4 100644
--- a/test-suite/bugs/closed/2378.v
+++ b/test-suite/bugs/closed/2378.v
@@ -63,7 +63,7 @@ Fixpoint lpSat st f: Prop :=
end.
End PropLogic.
-Implicit Arguments lpSat.
+Arguments lpSat : default implicits.
Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 :=
match f with
@@ -71,7 +71,7 @@ Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 :=
| LPAnd _ f1 f2 => LPAnd _ (LPTransfo Pred1 Pred2 p2lp f1) (LPTransfo Pred1 Pred2 p2lp f2)
| LPNot _ f1 => LPNot _ (LPTransfo Pred1 Pred2 p2lp f1)
end.
-Implicit Arguments LPTransfo.
+Arguments LPTransfo : default implicits.
Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f :=
LPTransfo (fun p => LPPred _ (existT (fun i => Pred i) i p)) f.
@@ -139,7 +139,7 @@ Definition trProd (State: Type) Ind (Pred: Ind -> Type) (tts: Ind -> TTS State)
{i:Ind & Pred i} -> LP (Predicate _ (TTSIndexedProduct _ Ind tts)) :=
fun p => addIndex Ind _ (projS1 p) (tr (projS1 p) (projS2 p)).
-Implicit Arguments trProd.
+Arguments trProd : default implicits.
Require Import Setoid.
Theorem satTrProd:
diff --git a/test-suite/bugs/closed/2404.v b/test-suite/bugs/closed/2404.v
index 8ac696e91..f6ec67601 100644
--- a/test-suite/bugs/closed/2404.v
+++ b/test-suite/bugs/closed/2404.v
@@ -22,13 +22,13 @@ Section Derived.
Definition bexportw := exportw base.
Definition bwweak := wweak base.
- Implicit Arguments bexportw [a b].
+ Arguments bexportw [a b].
Inductive RstarSetProof {I : Type} (T : I -> I -> Type) : I -> I -> Type :=
starReflS : forall a, RstarSetProof T a a
| starTransS : forall i j k, T i j -> (RstarSetProof T j k) -> RstarSetProof T i k.
-Implicit Arguments starTransS [I T i j k].
+Arguments starTransS [I T i j k].
Definition RstarInv {A : Set} (rel : relation A) : A -> A -> Type := (flip (RstarSetProof (flip rel))).
diff --git a/test-suite/bugs/closed/2584.v b/test-suite/bugs/closed/2584.v
index ef2e4e355..b5a723b47 100644
--- a/test-suite/bugs/closed/2584.v
+++ b/test-suite/bugs/closed/2584.v
@@ -8,7 +8,7 @@ Inductive res (A: Type) : Type :=
| OK: A -> res A
| Error: err -> res A.
-Implicit Arguments Error [A].
+Arguments Error [A].
Set Printing Universes.
diff --git a/test-suite/bugs/closed/2667.v b/test-suite/bugs/closed/2667.v
index 0631e5358..0e6d0108c 100644
--- a/test-suite/bugs/closed/2667.v
+++ b/test-suite/bugs/closed/2667.v
@@ -1,11 +1,11 @@
-(* Check that extra arguments to Arguments Scope do not disturb use of *)
+(* Check that extra arguments to Arguments do not disturb use of *)
(* scopes in constructors *)
Inductive stmt : Type := Sskip: stmt | Scall : nat -> stmt.
Bind Scope Cminor with stmt.
(* extra argument is ok because of possible coercion to funclass *)
-Arguments Scope Scall [_ Cminor ].
+Arguments Scall _ _%Cminor : extra scopes.
(* extra argument is ok because of possible coercion to funclass *)
Fixpoint f (c: stmt) : Prop := match c with Scall _ => False | _ => False end.
diff --git a/test-suite/bugs/closed/2729.v b/test-suite/bugs/closed/2729.v
index 7929b8810..c9d65c12c 100644
--- a/test-suite/bugs/closed/2729.v
+++ b/test-suite/bugs/closed/2729.v
@@ -82,8 +82,8 @@ Inductive SequenceBase (pu : PatchUniverse)
(p : pu_type from mid)
(qs : SequenceBase pu mid to),
SequenceBase pu from to.
-Implicit Arguments Nil [pu cxt].
-Implicit Arguments Cons [pu from mid to].
+Arguments Nil [pu cxt].
+Arguments Cons [pu from mid to].
Program Fixpoint insertBase {pu : PatchUniverse}
{from mid to : NameSet}
diff --git a/test-suite/bugs/closed/2830.v b/test-suite/bugs/closed/2830.v
index bb607b785..07a5cf91a 100644
--- a/test-suite/bugs/closed/2830.v
+++ b/test-suite/bugs/closed/2830.v
@@ -49,9 +49,9 @@ Record ageable_facts (A:Type) (level: A -> nat) (age1:A -> option A) :=
; af_level2 : forall x y, age1 x = Some y -> level x = S (level y)
}.
-Implicit Arguments af_unage [[A] [level] [age1]].
-Implicit Arguments af_level1 [[A] [level] [age1]].
-Implicit Arguments af_level2 [[A] [level] [age1]].
+Arguments af_unage {A level age1}.
+Arguments af_level1 {A level age1}.
+Arguments af_level2 {A level age1}.
Class ageable (A:Type) := mkAgeable
{ level : A -> nat
@@ -77,7 +77,7 @@ Coercion app_pred : pred >-> Funclass.
Global Opaque pred.
Definition derives {A} `{ageable A} (P Q:pred A) := forall a:A, P a -> Q a.
-Implicit Arguments derives.
+Arguments derives : default implicits.
Program Definition andp {A} `{ageable A} (P Q:pred A) : pred A :=
fun a:A => P a /\ Q a.
@@ -170,7 +170,7 @@ Class Functor `(C:Category) `(D:Category) (im : C -> D) := {
fmap g ∘ fmap f ≈ fmap (g ∘ f)
}.
Coercion functor_im : Functor >-> Funclass.
-Implicit Arguments fmap [Object Hom C Object0 Hom0 D im a b].
+Arguments fmap [Object Hom C Object0 Hom0 D im] _ [a b].
Add Parametric Morphism `(C:Category) `(D:Category)
(Im:C->D) (F:Functor C D Im) (a b:C) : (@fmap _ _ C _ _ D Im F a b)
diff --git a/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v
index 79671ce93..9811733dc 100644
--- a/test-suite/bugs/closed/3068.v
+++ b/test-suite/bugs/closed/3068.v
@@ -33,7 +33,7 @@ Section Counted_list.
End Counted_list.
-Implicit Arguments counted_def_nth [A n].
+Arguments counted_def_nth [A n].
Section Finite_nat_set.
diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
index 1f0f3b0da..a1d0b9107 100644
--- a/test-suite/bugs/closed/3513.v
+++ b/test-suite/bugs/closed/3513.v
@@ -21,7 +21,7 @@ Section ILogic_Fun.
Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit.
Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit.
End ILogic_Fun.
-Implicit Arguments ILFunFrm [[ILOps] [e]].
+Arguments ILFunFrm _ {e} _ {ILOps}.
Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q;
ltrue := True;
land P Q := P /\ Q;
diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v
index f5a22bd50..e91c004c7 100644
--- a/test-suite/bugs/closed/3647.v
+++ b/test-suite/bugs/closed/3647.v
@@ -26,7 +26,7 @@ Record morphism T T' `{e : type T} `{e' : type T'} :=
mkMorph {
morph :> T -> T';
morph_resp : setoid_resp morph}.
-Implicit Arguments mkMorph [T T' e e0 e' e1].
+Arguments mkMorph [T T' e0 e e1 e'].
Infix "-s>" := morphism (at level 45, right associativity).
Section Morphisms.
Context {S T U V} `{eS : type S} `{eT : type T} `{eU : type U} `{eV : type V}.
@@ -334,8 +334,8 @@ Section ILogic_Fun.
End ILogic_Fun.
-Implicit Arguments ILFunFrm [[ILOps] [e]].
-Implicit Arguments mkILFunFrm [T Frm ILOps].
+Arguments ILFunFrm _ {e} _ {ILOps}.
+Arguments mkILFunFrm [T] _ [Frm ILOps].
Program Definition ILFun_eq {T R} {ILOps: ILogicOps R} {ILogic: ILogic R} (P : T -> R) :
@ILFunFrm T _ R ILOps :=
diff --git a/test-suite/bugs/closed/3732.v b/test-suite/bugs/closed/3732.v
index 09f1149c2..13d62b8ff 100644
--- a/test-suite/bugs/closed/3732.v
+++ b/test-suite/bugs/closed/3732.v
@@ -16,7 +16,7 @@ Section machine.
| Inj : forall G, Prop -> propX G
| ExistsX : forall G A, propX (A :: G) -> propX G.
- Implicit Arguments Inj [G].
+ Arguments Inj [G].
Definition PropX := propX nil.
Fixpoint last (G : list Type) : Type.
diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v
index 8d7dfbd49..bc9380f90 100644
--- a/test-suite/bugs/closed/4095.v
+++ b/test-suite/bugs/closed/4095.v
@@ -23,7 +23,7 @@ Section ILogic_Fun.
Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit.
Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit.
End ILogic_Fun.
-Implicit Arguments ILFunFrm [[ILOps] [e]].
+Arguments ILFunFrm _ {e} _ {ILOps}.
Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q;
ltrue := True;
land P Q := P /\ Q;
diff --git a/test-suite/bugs/closed/4865.v b/test-suite/bugs/closed/4865.v
index c5bf3289b..da4e53aab 100644
--- a/test-suite/bugs/closed/4865.v
+++ b/test-suite/bugs/closed/4865.v
@@ -48,5 +48,5 @@ Fail Check g 0 0 1. (* 2nd 0 in bool *)
Fixpoint arr n := match n with 0%nat => nat | S n => nat -> arr n end.
Fixpoint lam n : arr n := match n with 0%nat => 0%nat | S n => fun x => lam n end.
Notation "0" := true.
-Arguments Scope lam [nat_scope nat_scope].
+Arguments lam _%nat_scope _%nat_scope : extra scopes.
Check (lam 1 0).
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 01:55:16 +0000