diff options
Diffstat (limited to 'test-suite')
28 files changed, 237 insertions, 77 deletions
diff --git a/test-suite/bugs/closed/bug_10939.v b/test-suite/bugs/closed/bug_10939.v new file mode 100644 index 0000000000..e4adc35554 --- /dev/null +++ b/test-suite/bugs/closed/bug_10939.v @@ -0,0 +1,5 @@ +Goal False. +Proof. + epose proof ltac:(shelve). (* works *) + epose proof ltac:(admit). (* anomaly *) +Abort. diff --git a/test-suite/bugs/closed/bug_12676.v b/test-suite/bugs/closed/bug_12676.v new file mode 100644 index 0000000000..5118ddb472 --- /dev/null +++ b/test-suite/bugs/closed/bug_12676.v @@ -0,0 +1,13 @@ + + +Definition nat_eq_dec(i j:nat) : {i=j}+{i<>j}. +Proof. + pose (diseq := false). + decide equality. +Defined. + +Set Mangle Names. +Definition nat_eq_dec_mangle (i j:nat) : {i=j}+{i<>j}. +Proof. + decide equality. (*Error: Anomaly "variable diseq unbound." ...*) +Defined. diff --git a/test-suite/bugs/closed/bug_12860.v b/test-suite/bugs/closed/bug_12860.v new file mode 100644 index 0000000000..243aeceba2 --- /dev/null +++ b/test-suite/bugs/closed/bug_12860.v @@ -0,0 +1,10 @@ +Require Import Coq.nsatz.NsatzTactic. +Require Import Coq.ZArith.ZArith Coq.QArith.QArith. + +Goal forall x y : Z, (x + y = y + x)%Z. + intros; nsatz. +Qed. + +Goal forall x y : Q, Qeq (x + y) (y + x). + intros; nsatz. +Qed. 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_12907.v b/test-suite/bugs/closed/bug_12907.v new file mode 100644 index 0000000000..4cd79cc1af --- /dev/null +++ b/test-suite/bugs/closed/bug_12907.v @@ -0,0 +1,7 @@ +From Coq Require Export Lia. +Set Mangle Names. +Lemma test (n : nat) : n <= 10 -> n <= 20. +Proof. lia. Qed. + +Lemma test2 : 0 < 1. +Proof. lia. Qed. 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_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_4095.v b/test-suite/bugs/closed/bug_4095.v index 3d3015c383..d667022e68 100644 --- a/test-suite/bugs/closed/bug_4095.v +++ b/test-suite/bugs/closed/bug_4095.v @@ -71,18 +71,9 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred) refine (P _ _) end. Undo. - Fail lazymatch goal with + lazymatch goal with | |- ?R (?f ?a ?b) (?f ?a' ?b') => let P := constr:(fun H H' => Morphisms.proper_prf a a' H b b' H') in set(p:=P) - end. (* Toplevel input, characters 15-182: -Error: Cannot infer an instance of type -"PointedOPred" for the variable p in environment: -T : Type -O0 : T -> OPred -O1 : T -> PointedOPred -tr : T -> T -O2 : PointedOPred -x0 : T -H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *) + end. Abort. 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-coqchk/bug_12845.out b/test-suite/output-coqchk/bug_12845.out new file mode 100644 index 0000000000..bef45bf2f6 --- /dev/null +++ b/test-suite/output-coqchk/bug_12845.out @@ -0,0 +1,14 @@ + +CONTEXT SUMMARY +=============== + +* Theory: Set is predicative + +* Axioms: <none> + +* Constants/Inductives relying on type-in-type: <none> + +* Constants/Inductives relying on unsafe (co)fixpoints: <none> + +* Inductives whose positivity is assumed: <none> + diff --git a/test-suite/output-coqchk/bug_12845.v b/test-suite/output-coqchk/bug_12845.v new file mode 100644 index 0000000000..d16146855b --- /dev/null +++ b/test-suite/output-coqchk/bug_12845.v @@ -0,0 +1,13 @@ +Module Type A. + Module B. + Axiom t : Set. + End B. +End A. + +Module a : A. + Module B. + Definition t : Set := unit. + End B. +End a. + +Check a.B.t. 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 2265028d3e..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) @@ -17,3 +17,7 @@ fix f (x : nat) : option nat := match x with | S _ => x end : nat -> option nat +fun x : False => let y := False_rect (A:=bool) x in y + : False -> bool +fun x : False => let y : True := False_rect x in y + : False -> True diff --git a/test-suite/output/Implicit.v b/test-suite/output/Implicit.v index a7c4399e38..86420bd8c8 100644 --- a/test-suite/output/Implicit.v +++ b/test-suite/output/Implicit.v @@ -61,3 +61,13 @@ Coercion some_nat := @Some nat. Check fix f x := match x with 0 => None | n => some_nat n end. End MatchBranchesInContext. + +Module LetInContext. + +Set Implicit Arguments. +Set Contextual Implicit. +Axiom False_rect : forall A:Type, False -> A. +Check fun x:False => let y:= False_rect (A:=bool) x in y. (* will not be in context: explicitation *) +Check fun x:False => let y:= False_rect (A:=True) x in y. (* will be in context: no explicitation *) + +End LetInContext. 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/Notations5.out b/test-suite/output/Notations5.out index f59306c454..a6c2553a89 100644 --- a/test-suite/output/Notations5.out +++ b/test-suite/output/Notations5.out @@ -146,8 +146,10 @@ v : forall (B : Type) (b : B), 0 = 0 /\ b = b @v 0 : forall (B : Type) (b : B), 0 = 0 /\ b = b -v 0 (B:=bool) +v 0 : forall b : bool, 0 = 0 /\ b = b + = ?n@{x:=v 0 (B:=bool)} + : nat v : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b v 0 @@ -166,8 +168,10 @@ v : forall (B : Type) (b : B), 0 = 0 /\ b = b @v 0 : forall (B : Type) (b : B), 0 = 0 /\ b = b -v 0 (B:=bool) +v 0 : forall b : bool, 0 = 0 /\ b = b + = ?n@{x:=v 0 (B:=bool)} + : nat ## : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b where @@ -192,10 +196,12 @@ where : 0 = 0 /\ true = true ## 0 0 true : 0 = 0 /\ true = true -## 0 0 (B:=bool) +## 0 0 : forall b : bool, 0 = 0 /\ b = b -## 0 0 (B:=bool) +## 0 0 : forall b : bool, 0 = 0 /\ b = b + = ?n@{x:=## 0 0 (B:=bool)} + : nat ## ?A : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b where @@ -230,10 +236,12 @@ where : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -## 0 0 (B:=bool) +## 0 0 : forall b : bool, 0 = 0 /\ b = b -## 0 0 (B:=bool) +## 0 0 : forall b : bool, 0 = 0 /\ b = b + = ?n@{x:=## 0 0 (B:=bool)} + : nat ## 0 0 true : 0 = 0 /\ true = true ## 0 0 true @@ -246,10 +254,12 @@ where : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -## 0 0 (B:=bool) +## 0 0 : forall b : bool, 0 = 0 /\ b = b -## 0 0 (B:=bool) +## 0 0 : forall b : bool, 0 = 0 /\ b = b + = ?n@{x:=## 0 0 (B:=bool)} + : nat ## 0 0 true : 0 = 0 /\ true = true ## 0 0 true diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v index 09d5e31c48..010b0da4a9 100644 --- a/test-suite/output/Notations5.v +++ b/test-suite/output/Notations5.v @@ -189,7 +189,9 @@ Module AppliedTermsPrinting. Check @v 0. (* @v 0 *) Check @p nat 0 0 bool. - (* v 0 (B:=bool) *) + (* v 0 *) + Eval simpl in (fun x => _:nat) (@p nat 0 0 bool). + (* ?n@{x:=v 0 (B:=bool)} *) End AtAbbreviationForPartialApplication. @@ -217,7 +219,9 @@ Module AppliedTermsPrinting. Check @v 0. (* @v 0 *) Check @p nat 0 0 bool. - (* v 0 (B:=bool) *) + (* v 0 *) + Eval simpl in (fun x => _:nat) (@p nat 0 0 bool). + (* ?n@{x:=v 0 (B:=bool)} *) End AbbreviationForPartialApplication. @@ -247,9 +251,11 @@ Module AppliedTermsPrinting. Check ## 0 0 true. (* ## 0 0 true *) Check p 0 0 (B:=bool). - (* ## 0 0 (B:=bool) *) + (* ## 0 0 *) Check ## 0 0 (B:=bool). - (* ## 0 0 (B:=bool) *) + (* ## 0 0 *) + Eval simpl in (fun x => _:nat) (@p nat 0 0 bool). + (* ?n@{x:=## 0 0 (B:=bool)} *) End NotationForHeadApplication. @@ -301,9 +307,11 @@ Module AppliedTermsPrinting. Check ## 0 0. (* ## 0 0 *) Check p 0 0 (B:=bool). - (* ## 0 0 (B:=bool) *) + (* ## 0 0 *) Check ## 0 0 (B:=bool). - (* ## 0 0 (B:=bool) *) + (* ## 0 0 *) + Eval simpl in (fun x => _:nat) (## 0 0 (B:=bool)). + (* ?n@{## 0 0 (B:=bool)} *) Check p 0 0 true. (* ## 0 0 true *) Check ## 0 0 true. @@ -327,9 +335,11 @@ Module AppliedTermsPrinting. Check ## 0 0. (* ## 0 0 *) Check p 0 0 (B:=bool). - (* ## 0 0 (B:=bool) *) + (* ## 0 0 *) Check ## 0 0 (B:=bool). - (* ## 0 0 (B:=bool) *) + (* ## 0 0 *) + Eval simpl in (fun x => _:nat) (## 0 0 (B:=bool)). + (* ?n@{## 0 0 (B:=bool)} *) Check p 0 0 true. (* ## 0 0 true *) Check ## 0 0 true. 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/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. |