diff options
Diffstat (limited to 'test-suite')
83 files changed, 333 insertions, 445 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/opened/1501.v b/test-suite/bugs/closed/1501.v index b36f21da1..e771e192d 100644 --- a/test-suite/bugs/opened/1501.v +++ b/test-suite/bugs/closed/1501.v @@ -3,6 +3,7 @@ Set Implicit Arguments. Require Export Relation_Definitions. Require Export Setoid. +Require Import Morphisms. Section Essais. @@ -40,57 +41,27 @@ Parameter Hint Resolve equiv_refl equiv_sym equiv_trans: monad. -Instance equiv_rel A: Equivalence (@equiv A). -Proof. - constructor. - intros xa; apply equiv_refl. - intros xa xb; apply equiv_sym. - intros xa xb xc; apply equiv_trans. -Defined. - -Definition fequiv (A B: Type) (f g: A -> K B) := forall (x:A), (equiv (f x) (g -x)). - -Lemma fequiv_refl : forall (A B: Type) (f : A -> K B), fequiv f f. -Proof. - unfold fequiv; auto with monad. -Qed. - -Lemma fequiv_sym : forall (A B: Type) (x y : A -> K B), fequiv x y -> fequiv y -x. -Proof. - unfold fequiv; auto with monad. -Qed. +Add Parametric Relation A : (K A) (@equiv A) + reflexivity proved by (@equiv_refl A) + symmetry proved by (@equiv_sym A) + transitivity proved by (@equiv_trans A) + as equiv_rel. -Lemma fequiv_trans : forall (A B: Type) (x y z : A -> K B), fequiv x y -> -fequiv -y z -> fequiv x z. +Add Parametric Morphism A B : (@bind A B) + with signature (@equiv A) ==> (pointwise_relation A (@equiv B)) ==> (@equiv B) + as bind_mor. Proof. - unfold fequiv; intros; eapply equiv_trans; auto with monad. -Qed. - -Instance fequiv_re A B: Equivalence (@fequiv A B). -Proof. - constructor. - intros f; apply fequiv_refl. - intros f g; apply fequiv_sym. - intros f g h; apply fequiv_trans. -Defined. - -Instance bind_mor A B: Morphisms.Proper (@equiv _ ==> @fequiv _ _ ==> @equiv _) (@bind A B). -Proof. - unfold fequiv; intros x y xy_equiv f g fg_equiv; apply bind_compat; auto. + unfold pointwise_relation; intros; apply bind_compat; auto. Qed. Lemma test: forall (A B: Type) (m1 m2 m3: K A) (f: A -> A -> K B), - (equiv m1 m2) -> (equiv m2 m3) -> - equiv (bind m1 (fun a => bind m2 (fun a' => f a a'))) - (bind m2 (fun a => bind m3 (fun a' => f a a'))). + (equiv m1 m2) -> (equiv m2 m3) -> + equiv (bind m1 (fun a => bind m2 (fun a' => f a a'))) + (bind m2 (fun a => bind m3 (fun a' => f a a'))). Proof. intros A B m1 m2 m3 f H1 H2. setoid_rewrite H1. (* this works *) - Fail setoid_rewrite H2. -Abort. -(* trivial by equiv_refl. -Qed.*) + setoid_rewrite H2. + reflexivity. +Qed. 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/opened/2456.v b/test-suite/bugs/closed/2456.v index 6cca5c9fb..e5a392c4d 100644 --- a/test-suite/bugs/opened/2456.v +++ b/test-suite/bugs/closed/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}, @@ -50,4 +50,9 @@ Fail dependent destruction commute1; dependent destruction catchCommuteDetails; dependent destruction commute2; dependent destruction catchCommuteDetails generalizing X. -Admitted. +revert X. +dependent destruction commute1; +dependent destruction catchCommuteDetails; +dependent destruction commute2; +dependent destruction catchCommuteDetails. +Abort. 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/opened/2814.v b/test-suite/bugs/closed/2814.v index a740b4384..99da1e3e4 100644 --- a/test-suite/bugs/opened/2814.v +++ b/test-suite/bugs/closed/2814.v @@ -3,3 +3,4 @@ Require Import Program. Goal forall (x : Type) (f g : Type -> Type) (H : f x ~= g x), False. intros. Fail induction H. +Abort. 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/opened/3100.v b/test-suite/bugs/closed/3100.v index 6f35a74dc..6f35a74dc 100644 --- a/test-suite/bugs/opened/3100.v +++ b/test-suite/bugs/closed/3100.v diff --git a/test-suite/bugs/opened/3230.v b/test-suite/bugs/closed/3230.v index 265310b1a..265310b1a 100644 --- a/test-suite/bugs/opened/3230.v +++ b/test-suite/bugs/closed/3230.v diff --git a/test-suite/bugs/opened/3320.v b/test-suite/bugs/closed/3320.v index 05cf73281..0aac3c1b0 100644 --- a/test-suite/bugs/opened/3320.v +++ b/test-suite/bugs/closed/3320.v @@ -2,3 +2,4 @@ Goal forall x : nat, True. fix 1. assumption. Fail Qed. +Undo. 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). diff --git a/test-suite/bugs/closed/6956.v b/test-suite/bugs/closed/6956.v new file mode 100644 index 000000000..ee21adbbf --- /dev/null +++ b/test-suite/bugs/closed/6956.v @@ -0,0 +1,13 @@ +(** Used to trigger an anomaly with VM compilation *) + +Set Universe Polymorphism. + +Inductive t A : nat -> Type := +| nil : t A 0 +| cons : forall (h : A) (n : nat), t A n -> t A (S n). + +Definition case0 {A} (P : t A 0 -> Type) (H : P (nil A)) v : P v := +match v with +| nil _ => H +| _ => fun devil => False_ind (@IDProp) devil +end. diff --git a/test-suite/bugs/closed/7092.v b/test-suite/bugs/closed/7092.v new file mode 100644 index 000000000..d90de8b93 --- /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/3209.v b/test-suite/bugs/opened/3209.v deleted file mode 100644 index 3203afa13..000000000 --- a/test-suite/bugs/opened/3209.v +++ /dev/null @@ -1,17 +0,0 @@ -Inductive eqT {A} (x : A) : A -> Type := - reflT : eqT x x. -Definition Bi_inv (A B : Type) (f : (A -> B)) := - sigT (fun (g : B -> A) => - sigT (fun (h : B -> A) => - sigT (fun (α : forall b : B, eqT (f (g b)) b) => - forall a : A, eqT (h (f a)) a))). -Definition TEquiv (A B : Type) := sigT (fun (f : A -> B) => Bi_inv _ _ f). - -Axiom UA : forall (A B : Type), TEquiv (TEquiv A B) (eqT A B). -Definition idtoeqv {A B} (e : eqT A B) : TEquiv A B := - sigT_rect (fun _ => TEquiv A B) - (fun (f : TEquiv A B -> eqT A B) H => - sigT_rect (fun _ => TEquiv A B) - (fun g _ => g e) - H) - (UA A B). diff --git a/test-suite/bugs/opened/3263.v b/test-suite/bugs/opened/3263.v deleted file mode 100644 index f0c707bd1..000000000 --- a/test-suite/bugs/opened/3263.v +++ /dev/null @@ -1,232 +0,0 @@ -Require Import TestSuite.admit. -(* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines, 2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *) -Generalizable All Variables. -Set Implicit Arguments. - -Arguments fst {_ _} _. -Arguments snd {_ _} _. - -Axiom cheat : forall {T}, T. - -Reserved Notation "g 'o' f" (at level 40, left associativity). - -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. -Arguments idpath {A a} , [A] a. -Notation "x = y" := (paths x y) : type_scope. - -Definition symmetry {A : Type} {x y : A} (p : x = y) : y = x - := match p with idpath => idpath end. - -Delimit Scope morphism_scope with morphism. -Delimit Scope category_scope with category. -Delimit Scope object_scope with object. -Record PreCategory (object : Type) := - Build_PreCategory' { - object :> Type := object; - morphism : object -> object -> Type; - identity : forall x, morphism x x; - compose : forall s d d', - morphism d d' - -> morphism s d - -> morphism s d' - where "f 'o' g" := (compose f g); - associativity : forall x1 x2 x3 x4 - (m1 : morphism x1 x2) - (m2 : morphism x2 x3) - (m3 : morphism x3 x4), - (m3 o m2) o m1 = m3 o (m2 o m1); - associativity_sym : forall x1 x2 x3 x4 - (m1 : morphism x1 x2) - (m2 : morphism x2 x3) - (m3 : morphism x3 x4), - m3 o (m2 o m1) = (m3 o m2) o m1; - left_identity : forall a b (f : morphism a b), identity b o f = f; - right_identity : forall a b (f : morphism a b), f o identity a = f; - identity_identity : forall x, identity x o identity x = identity x - }. -Bind Scope category_scope with PreCategory. -Arguments PreCategory {_}. -Arguments identity {_} [!C%category] x%object : rename. - -Arguments compose {_} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename. - -Infix "o" := compose : morphism_scope. - -Delimit Scope functor_scope with functor. -Local Open Scope morphism_scope. -Record Functor `(C : @PreCategory objC, D : @PreCategory objD) := - { - object_of :> C -> D; - morphism_of : forall s d, morphism C s d - -> morphism D (object_of s) (object_of d); - composition_of : forall s d d' - (m1 : morphism C s d) (m2: morphism C d d'), - morphism_of _ _ (m2 o m1) - = (morphism_of _ _ m2) o (morphism_of _ _ m1); - identity_of : forall x, morphism_of _ _ (identity x) - = identity (object_of x) - }. -Bind Scope functor_scope with Functor. - -Arguments morphism_of {_} [C%category] {_} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. - -Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope. - -Class IsIsomorphism `{C : @PreCategory objC} {s d} (m : morphism C s d) := - { - morphism_inverse : morphism C d s; - left_inverse : morphism_inverse o m = identity _; - right_inverse : m o morphism_inverse = identity _ - }. - -Definition opposite `(C : @PreCategory objC) : PreCategory - := @Build_PreCategory' - C - (fun s d => morphism C d s) - (identity (C := C)) - (fun _ _ _ m1 m2 => m2 o m1) - (fun _ _ _ _ _ _ _ => @associativity_sym _ _ _ _ _ _ _ _ _) - (fun _ _ _ _ _ _ _ => @associativity _ _ _ _ _ _ _ _ _) - (fun _ _ => @right_identity _ _ _ _) - (fun _ _ => @left_identity _ _ _ _) - (@identity_identity _ C). - -Notation "C ^op" := (opposite C) (at level 3) : category_scope. - -Definition prod `(C : @PreCategory objC, D : @PreCategory objD) : @PreCategory (objC * objD). - refine (@Build_PreCategory' - (C * D)%type - (fun s d => (morphism C (fst s) (fst d) - * morphism D (snd s) (snd d))%type) - (fun x => (identity (fst x), identity (snd x))) - (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1)) - _ - _ - _ - _ - _); admit. -Defined. -Infix "*" := prod : category_scope. - -Definition compose_functor `(C : @PreCategory objC, D : @PreCategory objD, E : @PreCategory objE) (G : Functor D E) (F : Functor C D) : Functor C E - := Build_Functor - C E - (fun c => G (F c)) - (fun _ _ m => morphism_of G (morphism_of F m)) - cheat - cheat. - -Infix "o" := compose_functor : functor_scope. - -Record NaturalTransformation `(C : @PreCategory objC, D : @PreCategory objD) (F G : Functor C D) := - Build_NaturalTransformation' { - components_of :> forall c, morphism D (F c) (G c); - commutes : forall s d (m : morphism C s d), - components_of d o F _1 m = G _1 m o components_of s; - - commutes_sym : forall s d (m : C.(morphism) s d), - G _1 m o components_of s = components_of d o F _1 m - }. -Definition functor_category `(C : @PreCategory objC, D : @PreCategory objD) : PreCategory - := @Build_PreCategory' (Functor C D) - (@NaturalTransformation _ C _ D) - cheat - cheat - cheat - cheat - cheat - cheat - cheat. - -Definition opposite_functor `(F : @Functor objC C objD D) : Functor C^op D^op - := Build_Functor (C^op) (D^op) - (object_of F) - (fun s d => morphism_of F (s := d) (d := s)) - (fun d' d s m1 m2 => composition_of F s d d' m2 m1) - (identity_of F). - -Definition opposite_invL `(F : @Functor objC C^op objD D) : Functor C D^op - := Build_Functor C (D^op) - (object_of F) - (fun s d => morphism_of F (s := d) (d := s)) - (fun d' d s m1 m2 => composition_of F s d d' m2 m1) - (identity_of F). -Notation "F ^op" := (opposite_functor F) : functor_scope. - -Notation "F ^op'L" := (opposite_invL F) (at level 3) : functor_scope. -Definition fst `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) C - := Build_Functor (C * D) C - (@fst _ _) - (fun _ _ => @fst _ _) - (fun _ _ _ _ _ => idpath) - (fun _ => idpath). - -Definition snd `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) D - := Build_Functor (C * D) D - (@snd _ _) - (fun _ _ => @snd _ _) - (fun _ _ _ _ _ => idpath) - (fun _ => idpath). -Definition prod_functor `(F : @Functor objC C objD D, F' : @Functor objC C objD' D') -: Functor C (D * D') - := Build_Functor - C (D * D') - (fun c => (F c, F' c)) - (fun s d m => (F _1 m, F' _1 m))%morphism - cheat - cheat. -Definition pair `(F : @Functor objC C objD D, F' : @Functor objC' C' objD' D') : Functor (C * C') (D * D') - := (prod_functor (F o fst) (F' o snd))%functor. -Notation cat_of obj := - (@Build_PreCategory' obj - (fun x y => forall _ : x, y) - (fun _ x => x) - (fun _ _ _ f g x => f (g x))%core - (fun _ _ _ _ _ _ _ => idpath) - (fun _ _ _ _ _ _ _ => idpath) - (fun _ _ _ => idpath) - (fun _ _ _ => idpath) - (fun _ => idpath)). - -Definition hom_functor `(C : @PreCategory objC) : Functor (C^op * C) (cat_of Type) - := Build_Functor _ _ cheat cheat cheat cheat. - -Definition induced_hom_natural_transformation `(F : @Functor objC C objD D) -: NaturalTransformation (hom_functor C) (hom_functor D o pair F^op F) - := Build_NaturalTransformation' _ _ cheat cheat cheat. - -Class IsFullyFaithful `(F : @Functor objC C objD D) - := is_fully_faithful - : forall x y : C, - IsIsomorphism (induced_hom_natural_transformation F (x, y)). - -Definition coyoneda `(A : @PreCategory objA) : Functor A^op (@functor_category _ A _ (cat_of Type)) - := cheat. - -Definition yoneda `(A : @PreCategory objA) : Functor A (@functor_category _ A^op _ (cat_of Type)) - := (((coyoneda A^op)^op'L)^op'L)%functor. -Definition coyoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@coyoneda _ A). -Admitted. - -Definition yoneda_embedding_fast `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). -Proof. - intros a b. - pose proof (coyoneda_embedding A^op a b) as CYE. - unfold yoneda. - Time let t := (type of CYE) in - let t' := (eval simpl in t) in pose proof ((fun (x : t) => (x : t')) CYE) as CYE'. (* Finished transaction in 0. secs (0.216013u,0.004s) *) - Fail Timeout 1 let t := match goal with |- ?G => constr:(G) end in - let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). - Time let t := match goal with |- ?G => constr:(G) end in - let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). (* Finished transaction in 0. secs (0.248016u,0.s) *) -Fail Timeout 2 Defined. -Time Defined. (* Finished transaction in 1. secs (0.432027u,0.s) *) - -Definition yoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). -Proof. - intros a b. - pose proof (coyoneda_embedding A^op a b) as CYE. - unfold yoneda; simpl in *. - Fail Timeout 1 exact CYE. - Time exact CYE. (* Finished transaction in 0. secs (0.012001u,0.s) *) -Fail Timeout 60 Defined. (* Timeout! *) diff --git a/test-suite/bugs/opened/3295.v b/test-suite/bugs/opened/3295.v index 2a156e333..c09649de7 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/bugs/opened/3916.v b/test-suite/bugs/opened/3916.v deleted file mode 100644 index fd95503e6..000000000 --- a/test-suite/bugs/opened/3916.v +++ /dev/null @@ -1,3 +0,0 @@ -Require Import List. - -Fail Hint Resolve -> in_map. (* Also happens when using <- instead of -> *) diff --git a/test-suite/bugs/opened/3948.v b/test-suite/bugs/opened/3948.v deleted file mode 100644 index 5c4b4277b..000000000 --- a/test-suite/bugs/opened/3948.v +++ /dev/null @@ -1,25 +0,0 @@ -Module Type S. -Parameter t : Type. -End S. - -Module Bar(X : S). -Proof. - Definition elt := X.t. - Axiom fold : elt. -End Bar. - -Module Make (X: S) := Bar(X). - -Declare Module X : S. - -Module Type Interface. - Parameter constant : unit. -End Interface. - -Module DepMap : Interface. - Module Dom := Make(X). - Definition constant : unit := - let _ := @Dom.fold in tt. -End DepMap. - -Print Assumptions DepMap.constant. diff --git a/test-suite/bugs/opened/4813.v b/test-suite/bugs/opened/4813.v index b75170179..2ac553593 100644 --- a/test-suite/bugs/opened/4813.v +++ b/test-suite/bugs/opened/4813.v @@ -1,5 +1,5 @@ -(* An example one would like to see succeeding *) +Require Import Program.Tactics. Record T := BT { t : Set }. Record U (x : T) := BU { u : t x -> Prop }. -Fail Definition A (H : unit -> Prop) : U (BT unit) := BU _ H. +Program Definition A (H : unit -> Prop) : U (BT unit) := BU _ H. diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v index 08f489d75..a76fa19d3 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/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index dc5a500db..88237815b 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -9,7 +9,15 @@ make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual + +# to learn about <(cmd) see https://www.gnu.org/software/bash/manual/html_node/Process-Substitution.html +( + while IFS= read -r -d '' d + do + pushd "$d" >/dev/null && find . && popd >/dev/null + done < <(find tmp -name user-contrib -print0) +) | sort -u > actual + sort -u > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index dc5a500db..5811dd17e 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -9,7 +9,13 @@ make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +( + while IFS= read -r -d '' d + do + pushd "$d" >/dev/null && find . && popd >/dev/null + done < <(find tmp -name user-contrib -print0) +) | sort -u > actual + sort -u > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/findlib-package/run.sh b/test-suite/coq-makefile/findlib-package/run.sh index 5b24df639..5cab400cc 100755 --- a/test-suite/coq-makefile/findlib-package/run.sh +++ b/test-suite/coq-makefile/findlib-package/run.sh @@ -7,7 +7,8 @@ export OCAMLPATH=$OCAMLPATH:$PWD/findlib if which cygpath 2>/dev/null; then # the only way I found to pass OCAMLPATH on win is to have it contain # only one entry - export OCAMLPATH=`cygpath -w $PWD/findlib` + OCAMLPATH=$(cygpath -w "$PWD"/findlib) + export OCAMLPATH fi make -C findlib/foo clean coq_makefile -f _CoqProject -o Makefile diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index 03df9cf05..bbd2fc460 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -8,7 +8,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib` && find .) | sort > actual +(cd "$(find tmp -name user-contrib)" && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index 03df9cf05..bbd2fc460 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -8,7 +8,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib` && find .) | sort > actual +(cd "$(find tmp -name user-contrib)" && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh index d3bb53106..45bf1481d 100755 --- a/test-suite/coq-makefile/multiroot/run.sh +++ b/test-suite/coq-makefile/multiroot/run.sh @@ -11,7 +11,12 @@ make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +( + while IFS= read -r -d '' d + do + pushd "$d" >/dev/null && find . && popd >/dev/null + done < <(find tmp -name user-contrib -print0) +) | sort -u > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 89bafe9ad..8f9ab9a71 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -1,17 +1,17 @@ #!/usr/bin/env bash -NATIVECOMP=`grep "let no_native_compiler = false" ../../../config/coq_config.ml`||true -if [[ `which ocamlopt` && $NATIVECOMP ]]; then +NATIVECOMP=$(grep "let no_native_compiler = false" ../../../config/coq_config.ml)||true +if [[ $(which ocamlopt) && $NATIVECOMP ]]; then . ../template/init.sh - + coq_makefile -f _CoqProject -o Makefile cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib` && find .) | sort > actual +(cd "$(find tmp -name user-contrib)" && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh index 5433d9e92..1e2bd979b 100755 --- a/test-suite/coq-makefile/plugin1/run.sh +++ b/test-suite/coq-makefile/plugin1/run.sh @@ -9,7 +9,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib` && find .) | sort > actual +(cd "$(find tmp -name user-contrib)" && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh index 5433d9e92..1e2bd979b 100755 --- a/test-suite/coq-makefile/plugin2/run.sh +++ b/test-suite/coq-makefile/plugin2/run.sh @@ -9,7 +9,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib` && find .) | sort > actual +(cd "$(find tmp -name user-contrib)" && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh index 5433d9e92..1e2bd979b 100755 --- a/test-suite/coq-makefile/plugin3/run.sh +++ b/test-suite/coq-makefile/plugin3/run.sh @@ -9,7 +9,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib` && find .) | sort > actual +(cd "$(find tmp -name user-contrib)" && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/quick2vo/run.sh b/test-suite/coq-makefile/quick2vo/run.sh index 9e681223b..dda51dd2e 100755 --- a/test-suite/coq-makefile/quick2vo/run.sh +++ b/test-suite/coq-makefile/quick2vo/run.sh @@ -1,11 +1,11 @@ #!/usr/bin/env bash -a=`uname` +a=$(uname) . ../template/init.sh coq_makefile -f _CoqProject -o Makefile # vio2vo is broken on Windows (#6720) -if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then +if [ "$a" = "Darwin" ] || [ "$a" = "Linux" ]; then make quick2vo J=2 test -f theories/test.vo make validate diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index e19d168cf..2e066d30d 100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -1,10 +1,11 @@ +#!/bin/sh . ../template/path-init.sh rm -rf _test mkdir _test find . -maxdepth 1 -not -name . -not -name _test -exec cp -r '{}' -t _test ';' -cd _test +cd _test || exit 1 mkdir -p src mkdir -p theories/sub diff --git a/test-suite/coq-makefile/template/path-init.sh b/test-suite/coq-makefile/template/path-init.sh index dd19ab2b1..c79b56652 100755 --- a/test-suite/coq-makefile/template/path-init.sh +++ b/test-suite/coq-makefile/template/path-init.sh @@ -1,3 +1,4 @@ +#!/bin/sh set -e set -o pipefail diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh index a918cceb6..9f3b648aa 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh @@ -4,7 +4,8 @@ set -x set -e cd "$(dirname "${BASH_SOURCE[0]}")" -export COQLIB="$(cd ../../../.. && pwd)" +COQLIB="$(cd ../../../.. && pwd)" +export COQLIB -./001-correct-diff-sorting-order/run.sh || exit $? -./002-single-file-sorting/run.sh || exit $? +./001-correct-diff-sorting-order/run.sh +./002-single-file-sorting/run.sh diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index aa6b0a9a4..11a04d5c2 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 @@ -58,16 +58,14 @@ TO_SED_IN_PER_LINE=( -e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs ) -for ext in "" .desired; do - for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do - cat ${file}${ext} | grep -v 'warning: undefined variable' | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed - done -done for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do - echo "cat $file" - cat "$file" - echo - diff -u $file.desired.processed $file.processed || exit $? + for ext in "" .desired; do + grep -v 'warning: undefined variable' < ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed + done + echo "cat $file" + cat "$file" + echo + diff -u $file.desired.processed $file.processed || exit $? done cd ../per-file-before @@ -92,13 +90,12 @@ echo "cat A.v.timing.diff" cat A.v.timing.diff echo +file=A.v.timing.diff + for ext in "" .desired; do - for file in A.v.timing.diff; do - cat ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" | sort > ${file}${ext}.processed - done -done -for file in A.v.timing.diff; do - diff -u $file.desired.processed $file.processed || exit $? + sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" < "${file}${ext}" | sort > "${file}${ext}.processed" done +diff -u "$file.desired.processed" "$file.processed" || exit $? + exit 0 diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh index 5354f794f..fc95d84b9 100755 --- a/test-suite/coq-makefile/uninstall1/run.sh +++ b/test-suite/coq-makefile/uninstall1/run.sh @@ -11,7 +11,12 @@ make install-doc DSTROOT="$PWD/tmp" make uninstall DSTROOT="$PWD/tmp" make uninstall-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +( + while IFS= read -r -d '' d + do + pushd "$d" >/dev/null && find . && popd >/dev/null + done < <(find tmp -name user-contrib -print0) +) | sort -u > actual sort -u > desired <<EOT . EOT diff --git a/test-suite/coq-makefile/uninstall2/run.sh b/test-suite/coq-makefile/uninstall2/run.sh index 5354f794f..fc95d84b9 100755 --- a/test-suite/coq-makefile/uninstall2/run.sh +++ b/test-suite/coq-makefile/uninstall2/run.sh @@ -11,7 +11,12 @@ make install-doc DSTROOT="$PWD/tmp" make uninstall DSTROOT="$PWD/tmp" make uninstall-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +( + while IFS= read -r -d '' d + do + pushd "$d" >/dev/null && find . && popd >/dev/null + done < <(find tmp -name user-contrib -print0) +) | sort -u > actual sort -u > desired <<EOT . EOT diff --git a/test-suite/coq-makefile/vio2vo/run.sh b/test-suite/coq-makefile/vio2vo/run.sh index 85656da41..e555d62f3 100755 --- a/test-suite/coq-makefile/vio2vo/run.sh +++ b/test-suite/coq-makefile/vio2vo/run.sh @@ -1,12 +1,12 @@ #!/usr/bin/env bash -a=`uname` +a=$(uname) . ../template/init.sh coq_makefile -f _CoqProject -o Makefile make quick # vio2vo is broken on Windows (#6720) -if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then +if [ "$a" = "Darwin" ] || [ "$a" = "Linux" ]; then make vio2vo J=2 test -f theories/test.vo make validate diff --git a/test-suite/failure/check.v b/test-suite/failure/check.v index a148ebe8e..0ef4b417a 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/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh index e07612b84..a15a8fbee 100755 --- a/test-suite/misc/deps-checksum.sh +++ b/test-suite/misc/deps-checksum.sh @@ -1,3 +1,4 @@ +#!/bin/sh rm -f misc/deps/A/*.vo misc/deps/B/*.vo $coqc -R misc/deps/A A misc/deps/A/A.v $coqc -R misc/deps/B A misc/deps/B/A.v diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh index 299f49469..6bb2ba2da 100755 --- a/test-suite/misc/deps-order.sh +++ b/test-suite/misc/deps-order.sh @@ -1,17 +1,18 @@ +#!/bin/sh # Check that both coqdep and coqtop/coqc supports -R # Check that both coqdep and coqtop/coqc takes the later -R # See bugs 2242, 2337, 2339 rm -f misc/deps/lib/*.vo misc/deps/client/*.vo -tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` -$coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput -diff -u --strip-trailing-cr misc/deps/deps.out $tmpoutput 2>&1 +tmpoutput=$(mktemp /tmp/coqcheck.XXXXXX) +$coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > "$tmpoutput" +diff -u --strip-trailing-cr misc/deps/deps.out "$tmpoutput" 2>&1 R=$? times $coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1 $coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1 $coqtop -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1 S=$? -if [ $R = 0 -a $S = 0 ]; then +if [ $R = 0 ] && [ $S = 0 ]; then printf "coqdep and coqtop agree\n" exit 0 else diff --git a/test-suite/misc/deps-utf8.sh b/test-suite/misc/deps-utf8.sh index 13e264c09..acb45b229 100755 --- a/test-suite/misc/deps-utf8.sh +++ b/test-suite/misc/deps-utf8.sh @@ -1,15 +1,16 @@ +#!/bin/sh # Check reading directories matching non pure ascii idents # See bug #5715 (utf-8 working on macos X and linux) # Windows is still not compliant -a=`uname` -if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then +a=$(uname) +if [ "$a" = "Darwin" ] || [ "$a" = "Linux" ]; then rm -f misc/deps/théorèmes/*.v -tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` +tmpoutput=$(mktemp /tmp/coqcheck.XXXXXX) $coqc -R misc/deps AlphaBêta misc/deps/αβ/γδ.v R=$? $coqtop -R misc/deps AlphaBêta -load-vernac-source misc/deps/αβ/εζ.v S=$? -if [ $R = 0 -a $S = 0 ]; then +if [ $R = 0 ] && [ $S = 0 ]; then exit 0 else exit 1 diff --git a/test-suite/misc/exitstatus.sh b/test-suite/misc/exitstatus.sh index cea1de862..a327f4248 100755 --- a/test-suite/misc/exitstatus.sh +++ b/test-suite/misc/exitstatus.sh @@ -1,7 +1,8 @@ +#!/bin/sh $coqtop -load-vernac-source misc/exitstatus/illtyped.v N=$? $coqc misc/exitstatus/illtyped.v P=$? -printf "On ill-typed input, coqtop returned $N.\n" -printf "On ill-typed input, coqc returned $P.\n" -if [ $N = 1 -a $P = 1 ]; then exit 0; else exit 1; fi +printf "On ill-typed input, coqtop returned %s.\n" "$N" +printf "On ill-typed input, coqc returned %s.\n" "$P" +if [ $N = 1 ] && [ $P = 1 ]; then exit 0; else exit 1; fi diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh index 28e7dc362..ef3f056d8 100755 --- a/test-suite/misc/printers.sh +++ b/test-suite/misc/printers.sh @@ -1,3 +1,2 @@ -printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound" -if [ $? = 0 ]; then exit 1; else exit 0; fi - +#!/bin/sh +if printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep -E "Error|Unbound" ; then exit 1; else exit 0; fi diff --git a/test-suite/misc/universes.sh b/test-suite/misc/universes.sh index d87a86035..ef61ca624 100755 --- a/test-suite/misc/universes.sh +++ b/test-suite/misc/universes.sh @@ -1,8 +1,9 @@ +#!/bin/sh # Sort universes for the whole standard library EXPECTED_UNIVERSES=4 # Prop is not counted $coqc -R misc/universes Universes misc/universes/all_stdlib 2>&1 $coqc -R misc/universes Universes misc/universes/universes 2>&1 mv universes.txt misc/universes -N=`awk '{print $3}' misc/universes/universes.txt | sort -u | wc -l` -printf "Found %s/%s universes\n" $N $EXPECTED_UNIVERSES +N=$(awk '{print $3}' misc/universes/universes.txt | sort -u | wc -l) +printf "Found %s/%s universes\n" "$N" "$EXPECTED_UNIVERSES" if [ "$N" -eq $EXPECTED_UNIVERSES ]; then exit 0; else exit 1; fi diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 8ba8525c6..be3310491 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 7214287a6..ece1b47b4 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/Notations3.out b/test-suite/output/Notations3.out index 1987b6a6e..304353f55 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -223,3 +223,11 @@ fun S : nat => [[S | S.S]] : Set exists2 '{{y, z}} : nat * nat, y > z & z > y : Prop +foo = +fun l : list nat => match l with + | _ :: (_ :: _) as l1 => l1 + | _ => l + end + : list nat -> list nat + +Argument scope is [list_scope] diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index c165f9553..d2d136946 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -278,10 +278,12 @@ Set Printing Notations. (* Check insensitivity of "match" clauses to order *) +Module IfPat. Notation "'if' t 'is' n .+ 1 'then' p 'else' q" := (match t with S n => p | 0 => q end) (at level 200). Check fun x => if x is n.+1 then n else 1. +End IfPat. (* Examples with binding patterns *) @@ -338,11 +340,13 @@ Check ∀ '(((x,y),true)|((x,y),false)), x>y. (* Check Georges' printability of a "if is then else" notation *) +Module IfPat2. Notation "'if' c 'is' p 'then' u 'else' v" := (match c with p => u | _ => v end) (at level 200, p pattern at level 100). Check fun p => if p is S n then n else 0. Check fun p => if p is Lt then 1 else 0. +End IfPat2. (* Check that mixed binders and terms defaults to ident and not pattern *) Module F. @@ -364,3 +368,15 @@ Check {'(x,y)|x+y=0}. (* Check exists2 with a pattern *) Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). + +Module Issue7110. +Open Scope list_scope. +Notation "[ :: x1 , x2 , .. , xn & s ]" := (x1 :: x2 :: .. (xn :: s) ..) + (at level 0). +Definition foo (l : list nat) := + match l with + | a :: (b :: l) as l1 => l1 + | _ => l +end. +Print foo. +End Issue7110. diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out new file mode 100644 index 000000000..e9c28faf1 --- /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 000000000..098a518dc --- /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 91ceb1b58..d6056c509 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 000000000..05464755f --- /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 000000000..bbe6b1a00 --- /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/output/ssr_clear.out b/test-suite/output/ssr_clear.out new file mode 100644 index 000000000..151595406 --- /dev/null +++ b/test-suite/output/ssr_clear.out @@ -0,0 +1,3 @@ +The command has indeed failed with message: +Ltac call to "move (ssrmovearg) (ssrclauses)" failed. +No assumption is named NO_SUCH_NAME diff --git a/test-suite/output/ssr_clear.v b/test-suite/output/ssr_clear.v new file mode 100644 index 000000000..573ec47e0 --- /dev/null +++ b/test-suite/output/ssr_clear.v @@ -0,0 +1,6 @@ +Require Import ssreflect. + +Example foo : True -> True. +Proof. +Fail move=> {NO_SUCH_NAME}. +Abort. diff --git a/test-suite/prerequisite/make_local.v b/test-suite/prerequisite/make_local.v index 8700a6c4e..6d9117c05 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 b4efa7edc..d0aa5c857 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 921433cad..9a19b595e 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 5b1482fd5..f07c0191f 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 45c71615f..ca8da3948 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 841940492..29350d620 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 6f27c1d36..18ebcd638 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 ca3746716..2da630633 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 cd6eac35c..400479ae8 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 02e043bc3..b287b5fac 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 bbfe5ec42..49a8b9cf4 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 f5bb884d2..55ae54ca0 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 627794832..5b13f35d5 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 a0981311b..23853890d 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. |