diff options
Diffstat (limited to 'test-suite')
49 files changed, 204 insertions, 66 deletions
diff --git a/test-suite/bugs/closed/1341.v b/test-suite/bugs/closed/1341.v index 8c5a38859f..79a0a14d7c 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 17eeb35291..c41e45900a 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 685811176a..5024a5bc97 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 7558b0b86d..e950554c4b 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 99952682d5..a3d9429307 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 febb9c7bb0..10e86cd12d 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 23a58501f3..6d73d58d4e 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 8ac696e912..f6ec676014 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 ef2e4e3555..b5a723b47f 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 0631e5358d..0e6d0108cc 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 7929b88108..c9d65c12c7 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 bb607b785b..07a5cf91a5 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 79671ce930..9811733dc6 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 1f0f3b0da9..a1d0b9107b 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 f5a22bd508..e91c004c77 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 09f1149c20..13d62b8ff6 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 8d7dfbd49b..bc9380f90d 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 c5bf3289bb..da4e53aab0 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). diff --git a/test-suite/bugs/closed/6631.v b/test-suite/bugs/closed/6631.v new file mode 100644 index 0000000000..100dc13fc8 --- /dev/null +++ b/test-suite/bugs/closed/6631.v @@ -0,0 +1,7 @@ +Require Import Coq.derive.Derive. + +Derive f SuchThat (f = 1 + 1) As feq. +Proof. + transitivity 2; [refine (eq_refl 2)|]. + transitivity 2. + 2:abstract exact (eq_refl 2). diff --git a/test-suite/bugs/closed/7092.v b/test-suite/bugs/closed/7092.v new file mode 100644 index 0000000000..d90de8b932 --- /dev/null +++ b/test-suite/bugs/closed/7092.v @@ -0,0 +1,70 @@ +(* Examples matching fix/cofix in Ltac pattern-matching *) + +Goal True. +lazymatch (eval cbv delta [Nat.add] in Nat.add) with +| (fix F (n : nat) (v : ?A) {struct n} : @?P n v + := match n with + | O => @?O_case v + | S n' => @?S_case n' v F + end) + => + unify A nat; + unify P (fun _ _ : nat => nat); + unify O_case (fun v : nat => v); + unify S_case (fun (p : nat) (m : nat) (add : nat -> nat -> nat) + => S (add p m)) + end. +Abort. + +Fixpoint f l n := match n with 0 => 0 | S n => g n (cons n l) end +with g n l := match n with 0 => 1 | S n => f (cons 0 l) n end. + +Goal True. + +lazymatch (eval cbv delta [f] in f) with +| fix myf (l : ?L) (n : ?N) {struct n} : nat := + match n as _ with + | 0 => ?Z + | S n0 => @?S myf myg n0 l + end + with myg (n' : ?N') (l' : ?L') {struct n'} : nat := + match n' as _ with + | 0 => ?Z' + | S n0' => @?S' myf myg n0' l' + end + for myf => + unify L (list nat); + unify L' (list nat); + unify N nat; + unify N' nat; + unify Z 0; + unify Z' 1; + unify S (fun (f : L -> N -> nat) (g : N -> L -> nat) n l => g n (cons n l)); + unify S' (fun (f : L -> N -> nat) (g : N -> L -> nat) (n:N) l => f (cons 0 l) n) +end. + +Abort. + +CoInductive S1 := C1 : nat -> S2 -> S1 with S2 := C2 : bool -> S1 -> S2. + +CoFixpoint f' n l := C1 n (g' (cons n l) n n) +with g' l n p := C2 true (f' (S n) l). + +Goal True. + +lazymatch (eval cbv delta [f'] in f') with +| cofix myf (n : ?N) (l : ?L) : ?T := @?X n g l + with g (l' : ?L') (n' : ?N') (p' : ?N'') : ?T' := @?X' n' myf l' + for myf => + unify L (list nat); + unify L' (list nat); + unify N nat; + unify N' nat; + unify N'' nat; + unify T S1; + unify T' S2; + unify X (fun n g l => C1 n (g (cons n l) n n)); + unify X' (fun n f (l : list nat) => C2 true (f (S n) l)) +end. + +Abort. diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v index 6cca5c9fba..5294adefd3 100644 --- a/test-suite/bugs/opened/2456.v +++ b/test-suite/bugs/opened/2456.v @@ -6,7 +6,7 @@ Parameter Patch : nat -> nat -> Set. Inductive Catch (from to : nat) : Type := MkCatch : forall (p : Patch from to), Catch from to. -Implicit Arguments MkCatch [from to]. +Arguments MkCatch [from to]. Inductive CatchCommute5 : forall {from mid1 mid2 to : nat}, diff --git a/test-suite/bugs/opened/3295.v b/test-suite/bugs/opened/3295.v index 2a156e333a..c09649de73 100644 --- a/test-suite/bugs/opened/3295.v +++ b/test-suite/bugs/opened/3295.v @@ -5,7 +5,7 @@ Class lops := lmk_ops { weq: relation car }. -Implicit Arguments car []. +Arguments car : clear implicits. Coercion car: lops >-> Sortclass. @@ -23,7 +23,7 @@ Class ops := mk_ops { dot: forall n m p, mor n m -> mor m p -> mor n p }. Coercion mor: ops >-> Funclass. -Implicit Arguments ob []. +Arguments ob : clear implicits. Instance dot_weq `{ops} n m p: Proper (weq ==> weq ==> weq) (dot n m p). Proof. diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v index 08f489d751..a76fa19d3c 100644 --- a/test-suite/complexity/injection.v +++ b/test-suite/complexity/injection.v @@ -47,7 +47,7 @@ Parameter mkJoinmap : forall (key: Type) (t: Type) (j: joinable t), joinmap key j. Parameter ADMIT: forall p: Prop, p. -Implicit Arguments ADMIT [p]. +Arguments ADMIT [p]. Module Share. Parameter jb : joinable bool. diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index aa6b0a9a43..43c83e412a 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -40,7 +40,7 @@ INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected TO_SED_IN_BOTH=( -e s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" # Whether or not something shows up as ∞ depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent - -e s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent + -e s':|\s*N/A\s*$:| '"${INFINITY_REPLACEMENT}"':g' # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent -e s'/ *$//g' # the number of trailing spaces depends on how many digits percentages end up being; since this varies across runs, we remove trailing spaces -e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out -e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators diff --git a/test-suite/failure/check.v b/test-suite/failure/check.v index a148ebe8e6..0ef4b417a5 100644 --- a/test-suite/failure/check.v +++ b/test-suite/failure/check.v @@ -1,3 +1,3 @@ -Implicit Arguments eq [A]. +Arguments eq [A]. Fail Check (bool = true). diff --git a/test-suite/ide/bug7088.fake b/test-suite/ide/bug7088.fake new file mode 100644 index 0000000000..e2a2aa52a0 --- /dev/null +++ b/test-suite/ide/bug7088.fake @@ -0,0 +1,13 @@ +ADD { Arguments id T x : rename. } +ADD { Lemma foo : True. } +ADD here { Proof. } +ADD { exact 3. } +ADD { Qed. } +WAIT +EDIT_AT here +ADD { Arguments id FOO BAR : rename. } +ADD { exact I. } +ADD { Qed. } +ADD { Arguments id T x : assert. } +JOIN + diff --git a/test-suite/ide/load.fake b/test-suite/ide/load.fake new file mode 100644 index 0000000000..f6a7ef4dcb --- /dev/null +++ b/test-suite/ide/load.fake @@ -0,0 +1,11 @@ +ADD revert { Load "output/load/Load_noproof.v". } +ADD { Load "output/load/Load_proof.v". } +ADD { Fail Load "output/load/Load_openproof.v". } +WAIT +QUERY { Check f. } +QUERY { Check u. } +EDIT_AT revert +QUERY { Check f. } +QUERY { Fail Check u. } +JOIN + diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 8ba8525c66..be33104918 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -1,8 +1,8 @@ Set Implicit Arguments. Unset Strict Implicit. -Implicit Arguments fst. -Implicit Arguments snd. +Arguments fst : default implicits. +Arguments snd : default implicits. Module Type PO. Parameter T : Set. diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v index 7214287a6a..ece1b47b4f 100644 --- a/test-suite/modules/Przyklad.v +++ b/test-suite/modules/Przyklad.v @@ -1,7 +1,7 @@ Definition ifte (T : Set) (A B : Prop) (s : {A} + {B}) (th el : T) := if s then th else el. -Implicit Arguments ifte. +Arguments ifte : default implicits. Lemma Reflexivity_provable : forall (A : Set) (a : A) (s : {a = a} + {a <> a}), diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index 38d055b28e..24180c4553 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -8,3 +8,11 @@ Unable to unify "nat" with "True". The command has indeed failed with message: Ltac call to "instantiate ( (ident) := (lglob) )" failed. Instance is not well-typed in the environment of ?x. +The command has indeed failed with message: +Cannot infer the domain of the type of f. +The command has indeed failed with message: +Cannot infer the domain of the implicit parameter A of id whose type is +"Type". +The command has indeed failed with message: +Cannot infer the codomain of the type of f in environment: +x : nat diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v index 424d24801c..c9b5091347 100644 --- a/test-suite/output/Errors.v +++ b/test-suite/output/Errors.v @@ -25,3 +25,9 @@ eexists ?[x]. destruct H1 as [x1 H1]. Fail instantiate (x:=projT1 x1). Abort. + +(* Test some messages for non solvable evars *) + +Fail Goal forall a f, f a = 0. +Fail Goal forall f x, id f x = 0. +Fail Goal forall f P, P (f 0). diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out new file mode 100644 index 0000000000..e9c28faf1d --- /dev/null +++ b/test-suite/output/Projections.out @@ -0,0 +1,2 @@ +fun S : store => S.(store_funcs) + : store -> host_func diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v new file mode 100644 index 0000000000..098a518dc4 --- /dev/null +++ b/test-suite/output/Projections.v @@ -0,0 +1,11 @@ + +Set Printing Projections. + +Class HostFunction := host_func : Type. + +Section store. + Context `{HostFunction}. + Record store := { store_funcs : host_func }. +End store. + +Check (fun (S:@store nat) => S.(store_funcs)). diff --git a/test-suite/output/bug5778.out b/test-suite/output/bug5778.out index 91ceb1b583..d6056c5098 100644 --- a/test-suite/output/bug5778.out +++ b/test-suite/output/bug5778.out @@ -1,4 +1,4 @@ The command has indeed failed with message: -In nested Ltac calls to "c", "abs" and "abstract b ltac:(())", last call -failed. +In nested Ltac calls to "c", "abs", "abstract b ltac:(())", +"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed. The term "I" has type "True" which should be Set, Prop or Type. diff --git a/test-suite/output/bug6404.out b/test-suite/output/bug6404.out new file mode 100644 index 0000000000..05464755f0 --- /dev/null +++ b/test-suite/output/bug6404.out @@ -0,0 +1,4 @@ +The command has indeed failed with message: +In nested Ltac calls to "c", "abs", "transparent_abstract (tactic3)", +"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed. +The term "I" has type "True" which should be Set, Prop or Type. diff --git a/test-suite/output/bug6404.v b/test-suite/output/bug6404.v new file mode 100644 index 0000000000..bbe6b1a00f --- /dev/null +++ b/test-suite/output/bug6404.v @@ -0,0 +1,7 @@ +Ltac a _ := pose (I : I). +Ltac b _ := a (). +Ltac abs _ := transparent_abstract b (). +Ltac c _ := abs (). +Goal True. + Fail c (). +Abort. diff --git a/test-suite/prerequisite/make_local.v b/test-suite/prerequisite/make_local.v index 8700a6c4e2..6d9117c05c 100644 --- a/test-suite/prerequisite/make_local.v +++ b/test-suite/prerequisite/make_local.v @@ -2,8 +2,7 @@ Definition f (A:Type) (a:A) := a. -Local Arguments Scope f [type_scope type_scope]. -Local Implicit Arguments f [A]. +Local Arguments f [A]%type_scope _%type_scope. (* Used in ImportedCoercion.v to test the locality flag *) 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/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/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. |