diff options
Diffstat (limited to 'test-suite/bugs')
27 files changed, 465 insertions, 122 deletions
diff --git a/test-suite/bugs/closed/2245.v b/test-suite/bugs/closed/2245.v new file mode 100644 index 0000000000..f0162f3b27 --- /dev/null +++ b/test-suite/bugs/closed/2245.v @@ -0,0 +1,11 @@ +Module Type Test. + +Section Sec. +Variables (A:Type). +Context (B:Type). +End Sec. + +Fail Check B. (* used to be found !!! *) +Fail Check A. + +End Test. diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v index 85ad41d1cf..23a58501f3 100644 --- a/test-suite/bugs/closed/2378.v +++ b/test-suite/bugs/closed/2378.v @@ -505,8 +505,6 @@ Qed. Require Export Coq.Logic.FunctionalExtensionality. Print PLanguage. -Unset Standard Proposition Elimination Names. - Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): Transformation (PLanguage l1) (PLanguage l2) := mkTransformation (PLanguage l1) (PLanguage l2) diff --git a/test-suite/bugs/closed/2850.v b/test-suite/bugs/closed/2850.v deleted file mode 100644 index 64a93aeb00..0000000000 --- a/test-suite/bugs/closed/2850.v +++ /dev/null @@ -1,2 +0,0 @@ -Definition id {A} (x : A) := x. -Fail Compute id. diff --git a/test-suite/bugs/closed/3481.v b/test-suite/bugs/closed/3481.v index 89d476dcb1..38f03b166b 100644 --- a/test-suite/bugs/closed/3481.v +++ b/test-suite/bugs/closed/3481.v @@ -3,7 +3,7 @@ Set Implicit Arguments. Require Import Logic. Module NonPrim. -Local Set Record Elimination Schemes. +Local Set Nonrecursive Elimination Schemes. Record prodwithlet (A B : Type) : Type := pair' { fst : A; fst' := fst; snd : B }. @@ -21,7 +21,7 @@ End NonPrim. Global Set Universe Polymorphism. Global Set Asymmetric Patterns. -Local Set Record Elimination Schemes. +Local Set Nonrecursive Elimination Schemes. Local Set Primitive Projections. Record prod (A B : Type) : Type := diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index 5adc48215e..1f0f3b0da9 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -69,26 +69,6 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred) refine (P _ _) end; unfold Basics.flip. Focus 2. - Set Typeclasses Debug. - Set Typeclasses Legacy Resolution. - apply reflexivity. - (* Debug: 1.1: apply @IsPointed_catOP on -(IsPointed (exists x0 : Actions, (catOP ?Goal O2 : OPred) x0)) -Debug: 1.1.1.1: apply OPred_inhabited on (IsPointed (exists x0 : Actions, ?Goal x0)) -Debug: 1.1.2.1: apply OPred_inhabited on (IsPointed (exists x : Actions, O2 x)) -Debug: 2.1: apply @Equivalence_Reflexive on (Reflexive lentails) -Debug: 2.1.1: no match for (Equivalence lentails) , 5 possibilities -Debug: Backtracking after apply @Equivalence_Reflexive -Debug: 2.2: apply @PreOrder_Reflexive on (Reflexive lentails) -Debug: 2.2.1.1: apply @lentailsPre on (PreOrder lentails) -Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred) -*) - Undo. Unset Typeclasses Legacy Resolution. - Test Typeclasses Unique Solutions. - Test Typeclasses Unique Instances. - Show Existentials. - Set Typeclasses Debug Verbosity 2. - Set Printing All. (* As in 8.5, allow a shelved subgoal to remain *) apply reflexivity. diff --git a/test-suite/bugs/closed/3520.v b/test-suite/bugs/closed/3520.v index c981207e6b..ea122e521f 100644 --- a/test-suite/bugs/closed/3520.v +++ b/test-suite/bugs/closed/3520.v @@ -3,7 +3,7 @@ Set Primitive Projections. Record foo (A : Type) := { bar : Type ; baz := Set; bad : baz = bar }. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Record notprim : Prop := { irrel : True; relevant : nat }. diff --git a/test-suite/bugs/closed/3662.v b/test-suite/bugs/closed/3662.v index bd53389b4f..b8754bce98 100644 --- a/test-suite/bugs/closed/3662.v +++ b/test-suite/bugs/closed/3662.v @@ -1,6 +1,6 @@ Set Primitive Projections. Set Implicit Arguments. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Record prod A B := pair { fst : A ; snd : B }. Definition f : Set -> Type := fun x => x. diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v index c3c97d3f59..0d347b262d 100644 --- a/test-suite/bugs/closed/4785.v +++ b/test-suite/bugs/closed/4785.v @@ -1,5 +1,4 @@ Require Coq.Lists.List Coq.Vectors.Vector. -Require Coq.Compat.Coq85. Module A. Import Coq.Lists.List Coq.Vectors.Vector. @@ -21,12 +20,10 @@ Delimit Scope mylist_scope with mylist. Bind Scope mylist_scope with mylist. Arguments mynil {_}, _. Arguments mycons {_} _ _. -Notation " [] " := mynil (compat "8.5") : mylist_scope. Notation " [ ] " := mynil (format "[ ]") : mylist_scope. Notation " [ x ] " := (mycons x nil) : mylist_scope. Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. -Import Coq.Compat.Coq85. Locate Module VectorNotations. Import VectorDef.VectorNotations. @@ -35,11 +32,3 @@ Check []%mylist : mylist _. Check [ ]%mylist : mylist _. Check [ ]%list : list _. End A. - -Module B. -Import Coq.Compat.Coq85. - -Goal True. - idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *) -Abort. -End B. diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v deleted file mode 100644 index bbb34f465c..0000000000 --- a/test-suite/bugs/closed/4785_compat_85.v +++ /dev/null @@ -1,46 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.5") -*- *) -Require Coq.Lists.List Coq.Vectors.Vector. -Require Coq.Compat.Coq85. - -Module A. -Import Coq.Lists.List Coq.Vectors.Vector. -Import ListNotations. -Check [ ]%list : list _. -Import VectorNotations ListNotations. -Delimit Scope vector_scope with vector. -Check [ ]%vector : Vector.t _ _. -Check []%vector : Vector.t _ _. -Check [ ]%list : list _. -Fail Check []%list : list _. - -Goal True. - idtac; [ ]. (* Note that vector notations break the [ | .. | ] syntax of Ltac *) -Abort. - -Inductive mylist A := mynil | mycons (x : A) (xs : mylist A). -Delimit Scope mylist_scope with mylist. -Bind Scope mylist_scope with mylist. -Arguments mynil {_}, _. -Arguments mycons {_} _ _. -Notation " [] " := mynil (compat "8.5") : mylist_scope. -Notation " [ ] " := mynil (format "[ ]") : mylist_scope. -Notation " [ x ] " := (mycons x nil) : mylist_scope. -Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. - -Import Coq.Compat.Coq85. -Locate Module VectorNotations. -Import VectorDef.VectorNotations. - -Check []%vector : Vector.t _ _. -Check []%mylist : mylist _. -Check [ ]%mylist : mylist _. -Check [ ]%list : list _. -End A. - -Module B. -Import Coq.Compat.Coq85. - -Goal True. - idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *) -Abort. -End B. diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v index dbc3d46fce..6f2bcb9685 100644 --- a/test-suite/bugs/closed/4798.v +++ b/test-suite/bugs/closed/4798.v @@ -1,3 +1,3 @@ Check match 2 with 0 => 0 | S n => n end. -Notation "|" := 1 (compat "8.4"). +Notation "|" := 1 (compat "8.6"). Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v index 3be36d8475..39299883ad 100644 --- a/test-suite/bugs/closed/4873.v +++ b/test-suite/bugs/closed/4873.v @@ -1,6 +1,5 @@ Require Import Coq.Classes.Morphisms. Require Import Relation_Definitions. -Require Import Coq.Compat.Coq85. Fixpoint tuple' T n : Type := match n with diff --git a/test-suite/bugs/closed/5532.v b/test-suite/bugs/closed/5532.v new file mode 100644 index 0000000000..ee5446e548 --- /dev/null +++ b/test-suite/bugs/closed/5532.v @@ -0,0 +1,15 @@ +(* A wish granted by the new support for patterns in notations *) + +Local Notation mkmatch0 e p + := match e with + | p => true + | _ => false + end. +Local Notation "'mkmatch' [[ e ]] [[ p ]]" + := match e with + | p => true + | _ => false + end + (at level 0, p pattern). +Check mkmatch0 _ ((0, 0)%core). +Check mkmatch [[ _ ]] [[ ((0, 0)%core) ]]. diff --git a/test-suite/bugs/closed/6313.v b/test-suite/bugs/closed/6313.v new file mode 100644 index 0000000000..4d263c5a82 --- /dev/null +++ b/test-suite/bugs/closed/6313.v @@ -0,0 +1,64 @@ +(* Former open goals in nested proofs were lost *) + +(* This used to fail with "Incorrect number of goals (expected 1 tactic)." *) + +Inductive foo := a | b | c. +Goal foo -> foo. + intro x. + simple refine (match x with + | a => _ + | b => ltac:(exact b) + | c => _ + end); [exact a|exact c]. +Abort. + +(* This used to leave the goal on the shelf and fails at reflexivity *) + +Goal (True/\0=0 -> True) -> True. + intro f. + refine + (f ltac:(split; only 1:exact I)). + reflexivity. +Qed. + +(* The "Unshelve" used to not see the explicitly "shelved" goal *) + +Lemma f (b:comparison) : b=b. +refine (match b with + Eq => ltac:(shelve) + | Lt => ltac:(give_up) + | Gt => _ + end). +exact (eq_refl Gt). +Unshelve. +exact (eq_refl Eq). +Fail auto. (* Check that there are no more regular subgoals *) +Admitted. + +(* The "Unshelve" used to not see the explicitly "shelved" goal *) + +Lemma f2 (b:comparison) : b=b. +refine (match b with + Eq => ltac:(shelve) + | Lt => ltac:(give_up) + | Gt => _ + end). +Unshelve. (* Note: Unshelve puts goals at the end *) +exact (eq_refl Gt). +exact (eq_refl Eq). +Fail auto. (* Check that there are no more regular subgoals *) +Admitted. + +(* The "unshelve" used to not see the explicitly "shelved" goal *) + +Lemma f3 (b:comparison) : b=b. +unshelve refine (match b with + Eq => ltac:(shelve) + | Lt => ltac:(give_up) + | Gt => _ + end). +(* Note: unshelve puts goals at the beginning *) +exact (eq_refl Eq). +exact (eq_refl Gt). +Fail auto. (* Check that there are no more regular subgoals *) +Admitted. diff --git a/test-suite/bugs/closed/6529.v b/test-suite/bugs/closed/6529.v new file mode 100644 index 0000000000..8d90819998 --- /dev/null +++ b/test-suite/bugs/closed/6529.v @@ -0,0 +1,16 @@ +Require Import Vector Program. + +Program Definition append_nil_def := + forall A n (ls: t A n), append ls (nil A) = ls. (* Works *) + +Lemma append_nil : append_nil_def. (* Works *) +Proof. +Admitted. + +Program Lemma append_nil' : + forall A n (ls: t A n), append ls (nil A) = ls. +Abort. + +Fail Program Lemma append_nil'' : + forall A B n (ls: t A n), append ls (nil A) = ls. +(* Error: Anomaly "Evar ?X25 was not declared." Please report at http://coq.inria.fr/bugs/. *) diff --git a/test-suite/bugs/closed/6634.v b/test-suite/bugs/closed/6634.v new file mode 100644 index 0000000000..7f33afcc2f --- /dev/null +++ b/test-suite/bugs/closed/6634.v @@ -0,0 +1,6 @@ +From Coq Require Import ssreflect. + +Lemma normalizeP (p : tt = tt) : p = p. +Proof. +Fail move: {2} tt p. +Abort. diff --git a/test-suite/bugs/closed/6661.v b/test-suite/bugs/closed/6661.v new file mode 100644 index 0000000000..e88a3704d8 --- /dev/null +++ b/test-suite/bugs/closed/6661.v @@ -0,0 +1,259 @@ +(* -*- mode: coq; coq-prog-args: ("-noinit" "-indices-matter" "-w" "-notation-overridden,-deprecated-option") -*- *) +(* + The Coq Proof Assistant, version 8.7.1 (January 2018) + compiled on Jan 21 2018 15:02:24 with OCaml 4.06.0 + from commit 391bb5e196901a3a9426295125b8d1c700ab6992 + *) + + +Require Export Coq.Init.Notations. +Notation "'∏' x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) : type_scope. +Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) + (at level 200, x binder, y binder, right associativity). +Notation "A -> B" := (forall (_ : A), B) : type_scope. +Reserved Notation "p @ q" (at level 60, right associativity). +Reserved Notation "! p " (at level 50). + +Monomorphic Universe uu. +Monomorphic Universe uu0. +Monomorphic Universe uu1. +Constraint uu0 < uu1. + +Global Set Universe Polymorphism. +Global Set Polymorphic Inductive Cumulativity. +Global Unset Universe Minimization ToSet. + +Notation UU := Type (only parsing). +Notation UU0 := Type@{uu0} (only parsing). + +Global Set Printing Universes. + + Inductive unit : UU0 := tt : unit. + +Inductive paths@{i} {A:Type@{i}} (a:A) : A -> Type@{i} := idpath : paths a a. +Hint Resolve idpath : core . +Notation "a = b" := (paths a b) (at level 70, no associativity) : type_scope. + +Set Primitive Projections. +Set Nonrecursive Elimination Schemes. + +Record total2@{i} { T: Type@{i} } ( P: T -> Type@{i} ) : Type@{i} + := tpair { pr1 : T; pr2 : P pr1 }. + +Arguments tpair {_} _ _ _. +Arguments pr1 {_ _} _. +Arguments pr2 {_ _} _. + +Notation "'∑' x .. y , P" := (total2 (λ x, .. (total2 (λ y, P)) ..)) + (at level 200, x binder, y binder, right associativity) : type_scope. + +Definition foo (X:Type) (xy : @total2 X (λ _, X)) : X. + induction xy as [x y]. + exact x. +Defined. + +Unset Automatic Introduction. + +Definition idfun (T : UU) := λ t:T, t. + +Definition pathscomp0 {X : UU} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c. +Proof. + intros. induction e1. exact e2. +Defined. + +Hint Resolve @pathscomp0 : pathshints. + +Notation "p @ q" := (pathscomp0 p q). + +Definition pathsinv0 {X : UU} {a b : X} (e : a = b) : b = a. +Proof. + intros. induction e. exact (idpath _). +Defined. + +Notation "! p " := (pathsinv0 p). + +Definition maponpaths {T1 T2 : UU} (f : T1 -> T2) {t1 t2 : T1} + (e: t1 = t2) : f t1 = f t2. +Proof. + intros. induction e. exact (idpath _). +Defined. + +Definition map_on_two_paths {X Y Z : UU} (f : X -> Y -> Z) {x x' y y'} (ex : x = x') (ey: y = y') : + f x y = f x' y'. +Proof. + intros. induction ex. induction ey. exact (idpath _). +Defined. + + +Definition maponpathscomp0 {X Y : UU} {x1 x2 x3 : X} + (f : X -> Y) (e1 : x1 = x2) (e2 : x2 = x3) : + maponpaths f (e1 @ e2) = maponpaths f e1 @ maponpaths f e2. +Proof. + intros. induction e1. induction e2. exact (idpath _). +Defined. + +Definition maponpathsinv0 {X Y : UU} (f : X -> Y) + {x1 x2 : X} (e : x1 = x2) : maponpaths f (! e) = ! (maponpaths f e). +Proof. + intros. induction e. exact (idpath _). +Defined. + + + +Definition constr1 {X : UU} (P : X -> UU) {x x' : X} (e : x = x') : + ∑ (f : P x -> P x'), + ∑ (ee : ∏ p : P x, tpair _ x p = tpair _ x' (f p)), + ∏ (pp : P x), maponpaths pr1 (ee pp) = e. +Proof. + intros. induction e. + split with (idfun (P x)). + split with (λ p, idpath _). + unfold maponpaths. simpl. + intro. exact (idpath _). +Defined. + +Definition transportf@{i} {X : Type@{i}} (P : X -> Type@{i}) {x x' : X} + (e : x = x') : P x -> P x' := pr1 (constr1 P e). + +Lemma two_arg_paths_f@{i} {A : Type@{i}} {B : A -> Type@{i}} {C:Type@{i}} {f : ∏ a, B a -> C} {a1 b1 a2 b2} + (p : a1 = a2) (q : transportf B p b1 = b2) : f a1 b1 = f a2 b2. +Proof. + intros. induction p. induction q. exact (idpath _). +Defined. + +Definition iscontr@{i} (T:Type@{i}) : Type@{i} := ∑ cntr:T, ∏ t:T, t=cntr. + +Lemma proofirrelevancecontr {X : UU} (is : iscontr X) (x x' : X) : x = x'. +Proof. + intros. + induction is as [y fe]. + exact (fe x @ !(fe x')). +Defined. + + +Definition hfiber@{i} {X Y : Type@{i}} (f : X -> Y) (y : Y) : Type@{i} := total2 (λ x, f x = y). + +Definition hfiberpair {X Y : UU} (f : X -> Y) {y : Y} + (x : X) (e : f x = y) : hfiber f y := + tpair _ x e. + +Definition coconustot (T : UU) (t : T) := ∑ t' : T, t' = t. + +Definition coconustotpair (T : UU) {t t' : T} (e: t' = t) : coconustot T t + := tpair _ t' e. + +Lemma connectedcoconustot {T : UU} {t : T} (c1 c2 : coconustot T t) : c1 = c2. +Proof. + intros. + induction c1 as [x0 x]. + induction x. + induction c2 as [x1 y]. + induction y. + exact (idpath _). +Defined. + +Definition isweq@{i} {X Y : Type@{i}} (f : X -> Y) : Type@{i} := + ∏ y : Y, iscontr (hfiber f y). + +Lemma isProofIrrelevantUnit : ∏ x x' : unit, x = x'. +Proof. + intros. induction x. induction x'. exact (idpath _). +Defined. + +Lemma unitl0 : tt = tt -> coconustot _ tt. +Proof. + intros e. exact (coconustotpair unit e). +Defined. + +Lemma unitl1: coconustot _ tt -> tt = tt. +Proof. + intro cp. induction cp as [x t]. induction x. exact t. +Defined. + +Lemma unitl2: ∏ e : tt = tt, unitl1 (unitl0 e) = e. +Proof. + intros. unfold unitl0. simpl. exact (idpath _). +Defined. + +Lemma unitl3: ∏ e : tt = tt, e = idpath tt. +Proof. + intros. + + assert (e0 : unitl0 (idpath tt) = unitl0 e). + { simple refine (connectedcoconustot _ _). } + + set (e1 := maponpaths unitl1 e0). + + exact (! (unitl2 e) @ (! e1) @ (unitl2 (idpath _))). +Defined. + +Theorem iscontrpathsinunit (x x' : unit) : iscontr (x = x'). +Proof. + intros. + split with (isProofIrrelevantUnit x x'). + intros e'. + induction x. + induction x'. + simpl. + apply unitl3. +Qed. + +Lemma ifcontrthenunitl0 (e1 e2 : tt = tt) : e1 = e2. +Proof. + intros. + simple refine (proofirrelevancecontr _ _ _). + exact (iscontrpathsinunit tt tt). +Qed. + +Section isweqcontrtounit. + + Universe i. + + (* To see the bug, run it both with and without this constraint: *) + + (* Constraint uu0 < i. *) + + (* Without this constraint, we get i = uu0 in the next definition *) + Lemma isweqcontrtounit@{} {T : Type@{i}} (is : iscontr@{i} T) : isweq@{i} (λ _:T, tt). + Proof. + intros. intro y. induction y. + induction is as [c h]. + split with (hfiberpair@{i i i} _ c (idpath tt)). + intros ha. + induction ha as [x e]. + simple refine (two_arg_paths_f (h x) _). + simple refine (ifcontrthenunitl0 _ _). + Defined. + + (* + Explanation of the bug: + + With the constraint uu0 < i above we get: + + |= uu0 <= bug.3 + uu0 <= i + uu1 <= i + i <= bug.3 + + from this print statement: *) + + Print isweqcontrtounit. + + (* + + Without the constraint uu0 < i above we get: + + |= i <= bug.3 + uu0 = i + + Since uu0 = i is not inferred when we impose the constraint uu0 < i, + it is invalid to infer it when we don't. + + *) + + Context (X : Type@{uu1}). + + Check (@isweqcontrtounit X). (* detect a universe inconsistency *) + +End isweqcontrtounit. diff --git a/test-suite/bugs/closed/6677.v b/test-suite/bugs/closed/6677.v new file mode 100644 index 0000000000..99e47bb87c --- /dev/null +++ b/test-suite/bugs/closed/6677.v @@ -0,0 +1,5 @@ +Set Universe Polymorphism. + +Definition T@{i} := Type@{i}. +Fail Definition U@{i} := (T@{i} <: Type@{i}). +Fail Definition eqU@{i j} : @eq T@{j} U@{i} T@{i} := eq_refl. diff --git a/test-suite/bugs/closed/6774.v b/test-suite/bugs/closed/6774.v new file mode 100644 index 0000000000..9625af91f5 --- /dev/null +++ b/test-suite/bugs/closed/6774.v @@ -0,0 +1,7 @@ +(* Was an anomaly with ill-typed template polymorphism *) +Definition huh (b:bool) := if b then Set else Prop. +Definition lol b: huh b := + if b return huh b then nat else True. +Goal (lol true) * unit. +Fail generalize true. (* should fail with error, not anomaly *) +Abort. diff --git a/test-suite/bugs/closed/6775.v b/test-suite/bugs/closed/6775.v new file mode 100644 index 0000000000..206df23bce --- /dev/null +++ b/test-suite/bugs/closed/6775.v @@ -0,0 +1,43 @@ +(* Issue caused and fixed during the lifetime of #6775: unification + failing on partially applied cumulative inductives. *) + +Set Universe Polymorphism. + +Set Polymorphic Inductive Cumulativity. + +Unset Elimination Schemes. + +Inductive paths@{i} {A : Type@{i}} (a : A) : A -> Type@{i} := + idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. + +Arguments inverse {A x y} p : simpl nomatch. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. + +Arguments concat {A x y z} p q : simpl nomatch. + +Notation "1" := idpath. + +Reserved Notation "p @ q" (at level 20). +Notation "p @ q" := (concat p q). + +Reserved Notation "p ^" (at level 3, format "p '^'"). +Notation "p ^" := (inverse p). + +Definition concat_pV_p {A} {x y z : A} (p : x = z) (q : y = z) : + (p @ q^) @ q = p + := + (match q as i return forall p, (p @ i^) @ i = p with + idpath => + fun p => + match p with idpath => 1 end + end) p. diff --git a/test-suite/bugs/closed/6878.v b/test-suite/bugs/closed/6878.v new file mode 100644 index 0000000000..70f1b3127a --- /dev/null +++ b/test-suite/bugs/closed/6878.v @@ -0,0 +1,8 @@ + +Set Universe Polymorphism. +Module Type T. + Axiom foo : Prop. +End T. + +(** Used to anomaly *) +Fail Module M : T with Definition foo := Type. diff --git a/test-suite/bugs/closed/6910.v b/test-suite/bugs/closed/6910.v new file mode 100644 index 0000000000..5167a5364a --- /dev/null +++ b/test-suite/bugs/closed/6910.v @@ -0,0 +1,5 @@ +From Coq Require Import ssreflect ssrfun. + +(* We should be able to use Some_inj as a view: *) +Lemma foo (x y : nat) : Some x = Some y -> x = y. +Proof. by move/Some_inj. Qed. diff --git a/test-suite/bugs/closed/HoTT_coq_077.v b/test-suite/bugs/closed/HoTT_coq_077.v index 017780c1f3..f69c71a026 100644 --- a/test-suite/bugs/closed/HoTT_coq_077.v +++ b/test-suite/bugs/closed/HoTT_coq_077.v @@ -3,7 +3,7 @@ Set Implicit Arguments. Require Import Logic. Set Asymmetric Patterns. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Set Primitive Projections. Record prod (A B : Type) : Type := diff --git a/test-suite/bugs/closed/HoTT_coq_104.v b/test-suite/bugs/closed/HoTT_coq_104.v index 5bb7fa8c12..a6ff78d127 100644 --- a/test-suite/bugs/closed/HoTT_coq_104.v +++ b/test-suite/bugs/closed/HoTT_coq_104.v @@ -4,7 +4,7 @@ Require Import Logic. Global Set Universe Polymorphism. Global Set Asymmetric Patterns. -Local Set Record Elimination Schemes. +Local Set Nonrecursive Elimination Schemes. Local Set Primitive Projections. Record prod (A B : Type) : Type := diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v index 0b576db6b3..820022d995 100644 --- a/test-suite/bugs/opened/1596.v +++ b/test-suite/bugs/opened/1596.v @@ -2,7 +2,6 @@ Require Import Relations. Require Import FSets. Require Import Arith. Require Import Omega. -Unset Standard Proposition Elimination Names. Set Keyed Unification. diff --git a/test-suite/bugs/closed/3424.v b/test-suite/bugs/opened/3424.v index ee8cabf171..d1c5bb68f9 100644 --- a/test-suite/bugs/closed/3424.v +++ b/test-suite/bugs/opened/3424.v @@ -13,12 +13,12 @@ Notation "0" := (trunc_S minus_one) : trunc_scope. Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. Notation IsHProp := (IsTrunc minus_one). Notation IsHSet := (IsTrunc 0). -Set Refolding Reduction. Goal forall (A : Type) (a b : A) (H' : IsHSet A), { x : Type & IsHProp x }. Proof. intros. eexists. (* exact (H' a b). *) (* Undo. *) -apply (H' a b). +Fail apply (H' a b). +exact (H' a b). Qed. diff --git a/test-suite/bugs/opened/3926.v b/test-suite/bugs/opened/3926.v deleted file mode 100644 index cfad763572..0000000000 --- a/test-suite/bugs/opened/3926.v +++ /dev/null @@ -1,30 +0,0 @@ -Notation compose := (fun g f x => g (f x)). -Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. -Open Scope function_scope. -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. -Arguments idpath {A a} , [A] a. -Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end. -Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }. -Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. -Local Open Scope equiv_scope. -Axiom eisretr : forall {A B} (f : A -> B) `{IsEquiv A B f} x, f (f^-1 x) = x. -Generalizable Variables A B C f g. -Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (compose g f) | 1000 - := Build_IsEquiv A C (compose g f) (compose f^-1 g^-1). -Definition isequiv_homotopic {A B} (f : A -> B) {g : A -> B} `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g - := Build_IsEquiv _ _ g (f ^-1). -Global Instance isequiv_inverse {A B} (f : A -> B) `{IsEquiv A B f} : IsEquiv f^-1 | 10000 - := Build_IsEquiv B A f^-1 f. -Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C} - `{IsEquiv A B f} `{IsEquiv A C (g o f)} - : IsEquiv g. -Proof. - Unset Typeclasses Modulo Eta. - exact (isequiv_homotopic (compose (compose g f) f^-1) - (fun b => ap g (eisretr f b))) || fail "too early". - Undo. - Set Typeclasses Modulo Eta. - Set Typeclasses Dependency Order. - Set Typeclasses Debug. - Fail exact (isequiv_homotopic (compose (compose g f) f^-1) - (fun b => ap g (eisretr f b))). diff --git a/test-suite/bugs/opened/6602.v b/test-suite/bugs/opened/6602.v new file mode 100644 index 0000000000..3690adf90a --- /dev/null +++ b/test-suite/bugs/opened/6602.v @@ -0,0 +1,17 @@ +Require Import Omega. + +Lemma test_nat: + forall n, (5 + pred n <= 5 + n). +Proof. + intros. + zify. + omega. +Qed. + +Lemma test_N: + forall n, (5 + N.pred n <= 5 + n)%N. +Proof. + intros. + zify. + omega. +Qed. |