diff options
Diffstat (limited to 'test-suite')
23 files changed, 173 insertions, 50 deletions
diff --git a/test-suite/bugs/closed/bug_12889.v b/test-suite/bugs/closed/bug_12889.v new file mode 100644 index 0000000000..f53cb8272d --- /dev/null +++ b/test-suite/bugs/closed/bug_12889.v @@ -0,0 +1,28 @@ +Require Import Relations. +Require Import Setoid. +Require Import Ring_theory. +Require Import Ring_base. + +Section S1. +Variable R : Type. +Variable Rone Rzero : R. +Variable Rplus Rmult Rminus : R -> R -> R. +Variable Rneg : R -> R. + +Lemma my_ring_theory1 : @ring_theory R Rzero Rone Rplus Rmult Rminus Rneg (@eq +R). +Admitted. +Add Ring my_ring : my_ring_theory1. +End S1. + +Section S2. +Variable R : Type. +Variable Rone Rzero : R. +Variable Rplus Rmult Rminus : R -> R -> R. +Variable Rneg : R -> R. + +Lemma my_ring_theory2 : @ring_theory R Rzero Rone Rplus Rmult Rminus Rneg (@eq +R). +Admitted. +Add Ring my_ring : my_ring_theory2. +End S2. diff --git a/test-suite/bugs/closed/bug_12909.v b/test-suite/bugs/closed/bug_12909.v new file mode 100644 index 0000000000..fafb6a418f --- /dev/null +++ b/test-suite/bugs/closed/bug_12909.v @@ -0,0 +1,8 @@ +Module Type T. +Axiom A : Type. +End T. + +Module M. + Axiom A : SProp. +End M. +Fail Module N <: T := M. diff --git a/test-suite/bugs/closed/bug_12928.v b/test-suite/bugs/closed/bug_12928.v new file mode 100644 index 0000000000..2f4d1dd16d --- /dev/null +++ b/test-suite/bugs/closed/bug_12928.v @@ -0,0 +1,7 @@ + +Lemma test: forall (x:bool) (x: nat), nat. +Proof. intros y x; abstract (exact x). Qed. + +Set Mangle Names. +Lemma test': forall x : nat, nat. +Proof. intros x. abstract exact x. Qed. diff --git a/test-suite/bugs/closed/bug_12944.v b/test-suite/bugs/closed/bug_12944.v new file mode 100644 index 0000000000..d6720d9906 --- /dev/null +++ b/test-suite/bugs/closed/bug_12944.v @@ -0,0 +1,12 @@ + +Inductive vector A : nat -> Type := + |nil : vector A 0 + |cons : forall (h:A) (n:nat), vector A n -> vector A (S n). + +Global Set Mangle Names. + +Lemma vlookup_middle {A n} (v : vector A n) : True. +Proof. + induction v as [|?? IHv]. + all:exact I. +Qed. diff --git a/test-suite/bugs/closed/bug_3146.v b/test-suite/bugs/closed/bug_3146.v new file mode 100644 index 0000000000..c42e28818a --- /dev/null +++ b/test-suite/bugs/closed/bug_3146.v @@ -0,0 +1,5 @@ +Axiom x : True. +Goal nat -> nat. + intro x. + abstract (exact x). +Qed. diff --git a/test-suite/bugs/closed/bug_5703.v b/test-suite/bugs/closed/bug_5703.v new file mode 100644 index 0000000000..c6e9eab9a7 --- /dev/null +++ b/test-suite/bugs/closed/bug_5703.v @@ -0,0 +1,9 @@ +Class A := {}. +Instance a:A := {}. +Hint Extern 0 A => abstract (exact a) : typeclass_instances. +Lemma lem : A. +Proof. + let a := constr:(_:A) in + let b := type of a in + exact a. +Defined. diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 8cf0797b17..5d1da05809 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -43,7 +43,7 @@ forall {D1 C1 : Type}, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 pf is not universe polymorphic -Arguments pf {D1}%foo_scope {C1}%type_scope _ [D2 C2] : simpl never +Arguments pf {D1}%foo_scope {C1}%type_scope _ [D2 C2] _ _ : simpl never The reduction tactics never unfold pf pf is transparent Expands to: Constant Arguments.pf diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index c28bb14eb3..e46774f68a 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -13,21 +13,25 @@ where ?y : [ |- nat] Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -Arguments eq {A}%type_scope -Arguments eq_refl {B}%type_scope {y}, [B] _ -eq_refl : forall {A : Type} {x : A}, x = x +Arguments eq {A}%type_scope _ _ +Arguments eq_refl {B}%type_scope {y}, [_] _ + (where some original arguments have been renamed) +eq_refl : forall {B : Type} {y : B}, y = y eq_refl is not universe polymorphic -Arguments eq_refl {B}%type_scope {y}, [B] _ +Arguments eq_refl {B}%type_scope {y}, [_] _ + (where some original arguments have been renamed) Expands to: Constructor Coq.Init.Logic.eq_refl Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x -Arguments myEq _%type_scope -Arguments myrefl {C}%type_scope x : rename -myrefl : forall {B : Type} (x : A), B -> myEq B x x +Arguments myEq _%type_scope _ _ +Arguments myrefl {C}%type_scope x _ + (where some original arguments have been renamed) +myrefl : forall {C : Type} (x : A), C -> myEq C x x myrefl is not universe polymorphic -Arguments myrefl {C}%type_scope x : rename +Arguments myrefl {C}%type_scope x _ + (where some original arguments have been renamed) Expands to: Constructor Arguments_renaming.Test1.myrefl myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := @@ -37,11 +41,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename -myplus : forall {T : Type}, T -> nat -> nat -> nat +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope + (where some original arguments have been renamed) +myplus : forall {Z : Type}, Z -> nat -> nat -> nat myplus is not universe polymorphic -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope + (where some original arguments have been renamed) The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent @@ -51,12 +57,14 @@ Expands to: Constant Arguments_renaming.Test1.myplus Inductive myEq (A B : Type) (x : A) : A -> Prop := myrefl : B -> myEq A B x x -Arguments myEq (_ _)%type_scope -Arguments myrefl A%type_scope {C}%type_scope x : rename -myrefl : forall (A : Type) {B : Type} (x : A), B -> myEq A B x x +Arguments myEq (_ _)%type_scope _ _ +Arguments myrefl A%type_scope {C}%type_scope x _ + (where some original arguments have been renamed) +myrefl : forall (A : Type) {C : Type} (x : A), C -> myEq A C x x myrefl is not universe polymorphic -Arguments myrefl A%type_scope {C}%type_scope x : rename +Arguments myrefl A%type_scope {C}%type_scope x _ + (where some original arguments have been renamed) Expands to: Constructor Arguments_renaming.myrefl myrefl : forall (A C : Type) (x : A), C -> myEq A C x x @@ -68,11 +76,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename -myplus : forall {T : Type}, T -> nat -> nat -> nat +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope + (where some original arguments have been renamed) +myplus : forall {Z : Type}, Z -> nat -> nat -> nat myplus is not universe polymorphic -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope + (where some original arguments have been renamed) The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent @@ -87,6 +97,9 @@ The command has indeed failed with message: Argument number 3 is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ]. The command has indeed failed with message: +Argument z is a trailing implicit, so it can't be declared non maximal. +Please use { } instead of [ ]. +The command has indeed failed with message: Extra arguments: y. The command has indeed failed with message: Flag "rename" expected to rename A into R. diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 6001850046..13bda0c070 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -48,6 +48,7 @@ Check @myplus. Fail Arguments eq_refl {F g}, [H] k. Fail Arguments eq_refl {F}, [F] : rename. +Fail Arguments eq {A} x [_] : rename. Fail Arguments eq {A} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 6976610b22..da2fc90fc3 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -7,7 +7,7 @@ fix F (t : t) : P t := : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t -Arguments t_rect (_ _)%function_scope +Arguments t_rect (_ _)%function_scope _ = fun d : TT => match d with | {| f3 := b |} => b end @@ -26,7 +26,7 @@ match Nat.eq_dec x y with end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y -Arguments proj (_ _)%nat_scope _%function_scope +Arguments proj (_ _)%nat_scope _%function_scope _ _ foo = fix foo (A : Type) (l : list A) {struct l} : option A := match l with @@ -43,7 +43,7 @@ fun (A : Type) (x : I A) => match x with end : forall A : Type, I A -> A -Arguments uncast _%type_scope +Arguments uncast _%type_scope _ foo' = if A 0 then true else false : bool f = diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index d8b88b8c1c..781e8e13a3 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -Arguments d2 [x x]%nat_scope +Arguments d2 [x x]%nat_scope _ map id (1 :: nil) : list nat map id' (1 :: nil) diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index e6c2806433..8e10107673 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -7,7 +7,7 @@ l : list' A Unable to unify "list' (A * A)%type" with "list' A". Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x -Arguments foo _%type_scope -Arguments Foo _%type_scope +Arguments foo _%type_scope _ +Arguments Foo _%type_scope _ myprod unit bool : Set diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index da255e86cd..02e58775b5 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -2,7 +2,7 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} Arguments sig2 [A]%type_scope (_ _)%type_scope -Arguments exist2 [A]%type_scope (_ _)%function_scope +Arguments exist2 [A]%type_scope (_ _)%function_scope _ _ _ exists x : nat, x = x : Prop fun b : bool => if b then b else b diff --git a/test-suite/output/Partac.out b/test-suite/output/Partac.out new file mode 100644 index 0000000000..889e698fa2 --- /dev/null +++ b/test-suite/output/Partac.out @@ -0,0 +1,6 @@ +The command has indeed failed with message: +The term "false" has type "bool" while it is expected to have type "nat". +(for subgoal 1) +The command has indeed failed with message: +The term "0" has type "nat" while it is expected to have type "bool". +(for subgoal 2) diff --git a/test-suite/output/Partac.v b/test-suite/output/Partac.v new file mode 100644 index 0000000000..f579ee683b --- /dev/null +++ b/test-suite/output/Partac.v @@ -0,0 +1,6 @@ +Goal nat * bool. +Proof. + split. + Fail par: exact false. + Fail par: exact 0. +Abort. diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index bdfa8afb6a..b8daa69ad2 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -15,7 +15,7 @@ swap = fun (A B : Type) '(x, y) => (y, x) : forall A B : Type, A * B -> B * A -Arguments swap {A B}%type_scope +Arguments swap {A B}%type_scope _ fun (A B : Type) '(x, y) => swap (x, y) = (y, x) : forall A B : Type, A * B -> Prop forall (A B : Type) '(x, y), swap (x, y) = (y, x) diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 8fb267e343..fe16dba496 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,24 +1,24 @@ existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x} existT is template universe polymorphic on sigT.u0 sigT.u1 -Arguments existT [A]%type_scope _%function_scope +Arguments existT [A]%type_scope _%function_scope _ _ Expands to: Constructor Coq.Init.Specif.existT Inductive sigT (A : Type) (P : A -> Type) : Type := existT : forall x : A, P x -> {x : A & P x} Arguments sigT [A]%type_scope _%type_scope -Arguments existT [A]%type_scope _%function_scope +Arguments existT [A]%type_scope _%function_scope _ _ existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -Arguments eq {A}%type_scope -Arguments eq_refl {A}%type_scope {x}, [A] _ +Arguments eq {A}%type_scope _ _ +Arguments eq_refl {A}%type_scope {x}, [_] _ eq_refl : forall {A : Type} {x : A}, x = x eq_refl is not universe polymorphic -Arguments eq_refl {A}%type_scope {x}, [A] _ +Arguments eq_refl {A}%type_scope {x}, [_] _ Expands to: Constructor Coq.Init.Logic.eq_refl eq_refl : forall {A : Type} {x : A}, x = x @@ -54,7 +54,7 @@ Inductive le (n : nat) : nat -> Prop := Arguments le (_ _)%nat_scope Arguments le_n _%nat_scope -Arguments le_S {n}%nat_scope [m]%nat_scope +Arguments le_S {n}%nat_scope [m]%nat_scope _ comparison : Set comparison is not universe polymorphic @@ -80,8 +80,8 @@ Notation sym_eq := eq_sym Expands to: Notation Coq.Init.Logic.sym_eq Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -Arguments eq {A}%type_scope -Arguments eq_refl {A}%type_scope {x}, {A} _ +Arguments eq {A}%type_scope _ _ +Arguments eq_refl {A}%type_scope {x}, {_} _ n:nat Hypothesis of the goal context. diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out index 1dd89c9bcd..1cdb39b020 100644 --- a/test-suite/output/Projections.out +++ b/test-suite/output/Projections.out @@ -7,11 +7,11 @@ let B := A in fun (C : Type) (u : U A C) => (A, B, C, c _ _ u) let B := A in forall C : Type, U A C -> Type * Type * Type * (B * A * C) -Arguments a (_ _)%type_scope +Arguments a (_ _)%type_scope _ b = fun A : Type => let B := A in fun (C : Type) (u : U A C) => b _ _ u : forall A : Type, let B := A in forall (C : Type) (u : U A C), (A, B, C, c _ _ u) = (A, B, C, c _ _ u) -Arguments b (_ _)%type_scope +Arguments b (_ _)%type_scope _ diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index edd2c9674f..163ed15606 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -5,24 +5,24 @@ Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } PWrap has primitive projections with eta conversion. Arguments PWrap _%type_scope -Arguments pwrap _%type_scope +Arguments pwrap _%type_scope _ punwrap@{u} = fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p : forall A : Type@{u}, PWrap@{u} A -> A (* u |= *) -Arguments punwrap _%type_scope +Arguments punwrap _%type_scope _ Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } (* u |= *) Arguments RWrap _%type_scope -Arguments rwrap _%type_scope +Arguments rwrap _%type_scope _ runwrap@{u} = fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap : forall A : Type@{u}, RWrap@{u} A -> A (* u |= *) -Arguments runwrap _%type_scope +Arguments runwrap _%type_scope _ Wrap@{u} = fun A : Type@{u} => A : Type@{u} -> Type@{u} (* u |= *) @@ -87,12 +87,12 @@ Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } PWrap has primitive projections with eta conversion. Arguments PWrap _%type_scope -Arguments pwrap _%type_scope +Arguments pwrap _%type_scope _ punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A (* K |= *) punwrap is universe polymorphic -Arguments punwrap _%type_scope +Arguments punwrap _%type_scope _ punwrap is transparent Expands to: Constant UnivBinders.punwrap The command has indeed failed with message: diff --git a/test-suite/output/bug_12887.out b/test-suite/output/bug_12887.out new file mode 100644 index 0000000000..5ea7722bc6 --- /dev/null +++ b/test-suite/output/bug_12887.out @@ -0,0 +1,10 @@ +The command has indeed failed with message: +Cannot infer this placeholder of type "Type" in +environment: +Functor : (Type -> Type) -> Type +F : Type -> Type +fmap : forall A B : Type, (A -> B) -> F A -> F B +The command has indeed failed with message: +Cannot infer an existential variable of type "nat" in +environment: +R : nat -> Type diff --git a/test-suite/output/bug_12887.v b/test-suite/output/bug_12887.v new file mode 100644 index 0000000000..4208c3e8e9 --- /dev/null +++ b/test-suite/output/bug_12887.v @@ -0,0 +1,10 @@ +Arguments id {_} _. + +Fail Record Functor (F : Type -> Type) := { + fmap : forall A B, (A -> B) -> F A -> F B; + fmap_identity : fmap _ _ id = id; +}. + +Fail Inductive R (x:nat) := { y : R ltac:(clear x) }. + +Inductive R (x:nat) := { y : bool; z : R _ }. diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 73fe53c757..a39b17e1f1 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -196,3 +196,13 @@ Goal forall m n:nat, n=m. double induction m n. Abort. +(* Mentioned as part of bug #12944 *) + +Inductive test : Set := cons : forall (IHv : nat) (v : test), test. + +Goal test -> test. +induction 1 as [? IHv]. +Undo. +destruct 1 as [? IHv]. +exact IHv. (* Check that the name is granted *) +Qed. diff --git a/test-suite/success/name_mangling.v b/test-suite/success/name_mangling.v index e982414206..d99e407b0d 100644 --- a/test-suite/success/name_mangling.v +++ b/test-suite/success/name_mangling.v @@ -1,7 +1,6 @@ -(* -*- coq-prog-args: ("-mangle-names" "_") -*- *) +Set Mangle Names. (* Check that refine policy of redefining previous names make these names private *) -(* abstract can change names in the environment! See bug #3146 *) Goal True -> True. intro. @@ -58,7 +57,7 @@ Abort. Goal False -> False. intro H. -Fail abstract exact H. +abstract exact H. Abort. (* Variant *) @@ -70,12 +69,11 @@ Abort. (* Example from Jason *) -Goal False -> False. +Lemma lem1 : False -> False. intro H. (* Name H' is from Ltac here, so it preserves the privacy *) (* But abstract messes everything up *) -Fail let H' := H in abstract exact H'. -let H' := H in exact H'. +let H' := H in abstract exact H'. Qed. (* Variant *) @@ -111,7 +109,7 @@ Goal forall b : False, b = b. Fail destruct b0. Abort. -Goal forall b : False, b = b. +Lemma lem2 : forall b : False, b = b. now destruct b. Qed. End foo. |