diff options
Diffstat (limited to 'test-suite/bugs/closed')
27 files changed, 459 insertions, 12 deletions
diff --git a/test-suite/bugs/closed/2428.v b/test-suite/bugs/closed/2428.v new file mode 100644 index 0000000000..b398a76d91 --- /dev/null +++ b/test-suite/bugs/closed/2428.v @@ -0,0 +1,10 @@ +Axiom P : nat -> Prop. + +Definition myFact := forall x, P x. + +Hint Extern 1 (P _) => progress (unfold myFact in *). + +Lemma test : (True -> myFact) -> P 3. +Proof. + intros. debug eauto. +Qed. diff --git a/test-suite/bugs/closed/2670.v b/test-suite/bugs/closed/2670.v index c401420e94..791889b24b 100644 --- a/test-suite/bugs/closed/2670.v +++ b/test-suite/bugs/closed/2670.v @@ -15,6 +15,14 @@ Proof. refine (match e return _ with refl_equal => _ end). reflexivity. Undo 2. + (** Check insensitivity to alphabetic order *) + refine (match e as a in _ = b return _ with refl_equal => _ end). + reflexivity. + Undo 2. + (** Check insensitivity to alphabetic order *) + refine (match e as z in _ = y return _ with refl_equal => _ end). + reflexivity. + Undo 2. (* Next line similarly has a dependent and a non dependent solution *) refine (match e with refl_equal => _ end). reflexivity. diff --git a/test-suite/bugs/closed/2733.v b/test-suite/bugs/closed/2733.v index 832de4f913..24dd30b32e 100644 --- a/test-suite/bugs/closed/2733.v +++ b/test-suite/bugs/closed/2733.v @@ -16,6 +16,21 @@ match k,l with |B,l' => Bcons true (Ncons 0 l') end. +(* At some time, the success of trullynul was dependent on the name of + the variables! *) + +Definition trullynul2 k {a} (l : alt_list k a) := +match k,l with + |N,l' => Ncons 0 (Bcons true l') + |B,l' => Bcons true (Ncons 0 l') +end. + +Definition trullynul3 k {z} (l : alt_list k z) := +match k,l with + |N,l' => Ncons 0 (Bcons true l') + |B,l' => Bcons true (Ncons 0 l') +end. + Fixpoint app (P : forall {k k'}, alt_list k k' -> alt_list k k') {t1 t2} (l : alt_list t1 t2) {struct l}: forall {t3}, alt_list t2 t3 -> alt_list t1 t3 := match l with diff --git a/test-suite/bugs/closed/4202.v b/test-suite/bugs/closed/4202.v new file mode 100644 index 0000000000..522a3604a3 --- /dev/null +++ b/test-suite/bugs/closed/4202.v @@ -0,0 +1,10 @@ +Parameter g : nat -> Prop. +Axiom a : forall n, g (S n). +Lemma foo (H : True) : exists n, g n /\ g n. +eexists. +clear H. +split. +simple apply a. +(* goal is "g (S ?Goal0@ {H:=H})" while H has long ceased to exist *) +simpl. +Abort. diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index 117d6523a8..f8cedfff6e 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -23,7 +23,9 @@ Module Export Datatypes. Set Implicit Arguments. Notation nat := Coq.Init.Datatypes.nat. +Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. +Notation two := (S (S O)). Record prod (A B : Type) := pair { fst : A ; snd : B }. @@ -159,7 +161,7 @@ End Adjointify. (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), @@ -220,12 +222,12 @@ Section ORecursion. Definition O_indpaths {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o to O P == h o to O P) : g == h - := (fst (snd (extendable_to_O O 2) g h) p).1. + := (fst (snd (extendable_to_O O two) g h) p).1. Definition O_indpaths_beta {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P) : O_indpaths g h p (to O P x) = p x - := (fst (snd (extendable_to_O O 2) g h) p).2 x. + := (fst (snd (extendable_to_O O two) g h) p).2 x. End ORecursion. diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v index c3e0da1117..fd2380a070 100644 --- a/test-suite/bugs/closed/4533.v +++ b/test-suite/bugs/closed/4533.v @@ -17,7 +17,10 @@ Notation "A -> B" := (forall (_ : A), B) : type_scope. Module Export Datatypes. Set Implicit Arguments. Notation nat := Coq.Init.Datatypes.nat. + Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. + Notation one := (S O). + Notation two := (S one). Record prod (A B : Type) := pair { fst : A ; snd : B }. Notation "x * y" := (prod x y) : type_scope. Delimit Scope nat_scope with nat. @@ -109,7 +112,7 @@ Fixpoint ExtendableAlong@{i j k l} (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), @@ -160,17 +163,17 @@ Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses). Definition O_rec {P Q : Type} {Q_inO : In O Q} (f : P -> Q) : O P -> Q - := (fst (extendable_to_O O 1%nat) f).1. + := (fst (extendable_to_O O one) f).1. Definition O_rec_beta {P Q : Type} {Q_inO : In O Q} (f : P -> Q) (x : P) : O_rec f (to O P x) = f x - := (fst (extendable_to_O O 1%nat) f).2 x. + := (fst (extendable_to_O O one) f).2 x. Definition O_indpaths {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o to O P == h o to O P) : g == h - := (fst (snd (extendable_to_O O 2) g h) p).1. + := (fst (snd (extendable_to_O O two) g h) p).1. End ORecursion. diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index 4ad53bc629..13c47edc8f 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -19,6 +19,7 @@ Inductive sum (A B : Type) : Type := | inl : A -> sum A B | inr : B -> sum A B. Notation nat := Coq.Init.Datatypes.nat. +Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. Notation "x + y" := (sum x y) : type_scope. @@ -449,7 +450,7 @@ Section Extensions. (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), diff --git a/test-suite/bugs/closed/4623.v b/test-suite/bugs/closed/4623.v new file mode 100644 index 0000000000..7ecfd98b67 --- /dev/null +++ b/test-suite/bugs/closed/4623.v @@ -0,0 +1,5 @@ +Goal Type -> Type. +set (T := Type). +clearbody T. +refine (@id _). +Qed. diff --git a/test-suite/bugs/closed/4624.v b/test-suite/bugs/closed/4624.v new file mode 100644 index 0000000000..f5ce981cd0 --- /dev/null +++ b/test-suite/bugs/closed/4624.v @@ -0,0 +1,7 @@ +Record foo := mkfoo { type : Type }. + +Canonical Structure fooA (T : Type) := mkfoo (T -> T). + +Definition id (t : foo) (x : type t) := x. + +Definition bar := id _ ((fun x : nat => x) : _). diff --git a/test-suite/bugs/closed/4717.v b/test-suite/bugs/closed/4717.v index 1507fa4bf0..bd9bac37ef 100644 --- a/test-suite/bugs/closed/4717.v +++ b/test-suite/bugs/closed/4717.v @@ -19,8 +19,6 @@ Proof. omega. Qed. -Require Import ZArith ROmega. - Open Scope Z_scope. Definition Z' := Z. @@ -32,6 +30,4 @@ Theorem Zle_not_eq_lt : forall n m, Proof. intros. omega. - Undo. - romega. Qed. diff --git a/test-suite/bugs/closed/7333.v b/test-suite/bugs/closed/7333.v new file mode 100644 index 0000000000..fba5b9029d --- /dev/null +++ b/test-suite/bugs/closed/7333.v @@ -0,0 +1,39 @@ +Module Example1. + +CoInductive wrap : Type := + | item : unit -> wrap. + +Definition extract (t : wrap) : unit := +match t with +| item x => x +end. + +CoFixpoint close u : unit -> wrap := +match u with +| tt => item +end. + +Definition table : wrap := close tt tt. + +Eval vm_compute in (extract table). +Eval vm_compute in (extract table). + +End Example1. + +Module Example2. + +Set Primitive Projections. +CoInductive wrap : Type := + item { extract : unit }. + +CoFixpoint close u : unit -> wrap := +match u with +| tt => item +end. + +Definition table : wrap := close tt tt. + +Eval vm_compute in (extract table). +Eval vm_compute in (extract table). + +End Example2. diff --git a/test-suite/bugs/closed/7754.v b/test-suite/bugs/closed/7754.v new file mode 100644 index 0000000000..229df93773 --- /dev/null +++ b/test-suite/bugs/closed/7754.v @@ -0,0 +1,21 @@ + +Set Universe Polymorphism. + +Module OK. + + Inductive one@{i j} : Type@{i} := + with two : Type@{j} := . + Check one@{Set Type} : Set. + Fail Check two@{Set Type} : Set. + +End OK. + +Module Bad. + + Fail Inductive one := + with two@{i +} : Type@{i} := . + + Fail Inductive one@{i +} := + with two@{i +} := . + +End Bad. diff --git a/test-suite/bugs/closed/7795.v b/test-suite/bugs/closed/7795.v new file mode 100644 index 0000000000..5db0f81cc5 --- /dev/null +++ b/test-suite/bugs/closed/7795.v @@ -0,0 +1,65 @@ + + +Definition fwd (b: bool) A (e2: A): A. Admitted. + +Ltac destruct_refinement_aux T := + let m := fresh "mres" in + let r := fresh "r" in + let P := fresh "P" in + pose T as m; + destruct m as [ r P ]. + +Ltac destruct_refinement := + match goal with + | |- context[proj1_sig ?T] => destruct_refinement_aux T + end. + +Ltac t_base := discriminate || destruct_refinement. + + +Inductive List (T: Type) := +| Cons_construct: T -> List T -> List T +| Nil_construct: List T. + +Definition t (T: Type): List T. Admitted. +Definition size (T: Type) (src: List T): nat. Admitted. +Definition filter1_rt1_type (T: Type): Type := { res: List T | false = true }. +Definition filter1 (T: Type): filter1_rt1_type T. Admitted. + +Definition hh_1: + forall T : Type, + (forall (T0 : Type), + False -> filter1_rt1_type T0) -> + False. +Admitted. + +Definition hh_2: + forall (T : Type), + filter1_rt1_type T -> + filter1_rt1_type T. +Admitted. + +Definition hh: + forall (T : Type) (f1 : forall (T0 : Type), False -> filter1_rt1_type T0), + fwd + (Nat.leb + (size T + (fwd false (List T) + (fwd false (List T) + (proj1_sig + (hh_2 T + (f1 T (hh_1 T f1))))))) 0) bool + false = true. +Admitted. + +Set Program Mode. (* removing this line prevents the bug *) +Obligation Tactic := repeat t_base. + +Goal + forall T (h17: T), + filter1 T = + exist + _ + (Nil_construct T) + (hh T (fun (T : Type) (_ : False) => filter1 T)). +Abort. diff --git a/test-suite/bugs/closed/7854.v b/test-suite/bugs/closed/7854.v new file mode 100644 index 0000000000..ab1a29b632 --- /dev/null +++ b/test-suite/bugs/closed/7854.v @@ -0,0 +1,10 @@ +Set Primitive Projections. + +CoInductive stream (A : Type) := cons { + hd : A; + tl : stream A; +}. + +CoFixpoint const {A} (x : A) := cons A x (const x). + +Check (@eq_refl _ (const tt) <<: tl unit (const tt) = const tt). diff --git a/test-suite/bugs/closed/7867.v b/test-suite/bugs/closed/7867.v new file mode 100644 index 0000000000..d0c7902756 --- /dev/null +++ b/test-suite/bugs/closed/7867.v @@ -0,0 +1,4 @@ +(* Was a printer anomaly due to an internal lambda with no binders *) + +Class class := { foo : nat }. +Fail Instance : class := { foo := 0 ; bar := 0 }. diff --git a/test-suite/bugs/closed/7900.v b/test-suite/bugs/closed/7900.v new file mode 100644 index 0000000000..583ef0ef3b --- /dev/null +++ b/test-suite/bugs/closed/7900.v @@ -0,0 +1,53 @@ +Require Import Coq.Program.Program. +(* Set Universe Polymorphism. *) +Set Printing Universes. + +Axiom ALL : forall {T:Prop}, T. + +Inductive Expr : Set := E (a : Expr). + +Parameter Value : Set. + +Fixpoint eval (e: Expr): Value := + match e with + | E a => eval a + end. + +Class Quote (n: Value) : Set := + { quote: Expr + ; eval_quote: eval quote = n }. + +Program Definition quote_mult n + `{!Quote n} : Quote n := + {| quote := E (quote (n:=n)) |}. + +Set Printing Universes. +Next Obligation. +Proof. + Show Universes. + destruct Quote0 as [q eq]. + Show Universes. + rewrite <- eq. + clear n eq. + Show Universes. + apply ALL. + Show Universes. +Qed. +Print quote_mult_obligation_1. +(* quote_mult_obligation_1@{} = +let Top_internal_eq_rew_dep := + fun (A : Type@{Coq.Init.Logic.8}) (x : A) (P : forall a : A, x = a -> Type@{Top.5} (* <- XXX *)) + (f : P x eq_refl) (y : A) (e : x = y) => + match e as e0 in (_ = y0) return (P y0 e0) with + | eq_refl => f + end in +fun (n : Value) (Quote0 : Quote n) => +match Quote0 as q return (eval quote = n) with +| {| quote := q; eval_quote := eq0 |} => + Top_internal_eq_rew_dep Value (eval q) (fun (n0 : Value) (eq1 : eval q = n0) => eval quote = n0) + ALL n eq0 +end + : forall (n : Value) (Quote0 : Quote n), eval (E quote) = n + +quote_mult_obligation_1 is universe polymorphic +*) diff --git a/test-suite/bugs/closed/7967.v b/test-suite/bugs/closed/7967.v new file mode 100644 index 0000000000..2c8855fd54 --- /dev/null +++ b/test-suite/bugs/closed/7967.v @@ -0,0 +1,2 @@ +Set Universe Polymorphism. +Inductive A@{} : Set := B : ltac:(let y := constr:(Type) in exact nat) -> A. diff --git a/test-suite/bugs/closed/8081.v b/test-suite/bugs/closed/8081.v new file mode 100644 index 0000000000..0f2501aaa8 --- /dev/null +++ b/test-suite/bugs/closed/8081.v @@ -0,0 +1,4 @@ +Section foo. +End foo. +Section foo. +End foo. diff --git a/test-suite/bugs/closed/8106.v b/test-suite/bugs/closed/8106.v new file mode 100644 index 0000000000..a711c5adef --- /dev/null +++ b/test-suite/bugs/closed/8106.v @@ -0,0 +1,4 @@ +(* Was raising an anomaly "already assigned a level" on the second line *) + +Notation "c1 ; c2" := (c1 + c2) (only printing, at level 76, right associativity, c1 at level 76, c2 at level 76). +Notation "c1 ; c2" := (c1 + c2) (only parsing, at level 76, right associativity, c2 at level 76). diff --git a/test-suite/bugs/closed/8119.v b/test-suite/bugs/closed/8119.v new file mode 100644 index 0000000000..c6329a7328 --- /dev/null +++ b/test-suite/bugs/closed/8119.v @@ -0,0 +1,46 @@ +Require Import Coq.Strings.String. + +Section T. + Eval vm_compute in let x := tt in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Eval vm_compute in let _ := Set in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Eval vm_compute in let _ := Prop in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End T. + +Section U0. + Let n : unit := tt. + Eval vm_compute in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End U0. + +Section S0. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval vm_compute in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End S0. + +Class T := { }. +Section S1. + Context {p : T}. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval vm_compute in _. +(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort. +(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *) +End S1. + +Class M := { m : Type }. +Section S2. + Context {p : M}. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval vm_compute in _. +(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *) + Goal exists tt : unit, tt = tt. eexists. vm_compute. Abort. +(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *) +End S2. diff --git a/test-suite/bugs/closed/8121.v b/test-suite/bugs/closed/8121.v new file mode 100644 index 0000000000..99267612ca --- /dev/null +++ b/test-suite/bugs/closed/8121.v @@ -0,0 +1,46 @@ +Require Import Coq.Strings.String. + +Section T. + Eval native_compute in let x := tt in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Eval native_compute in let _ := Set in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Eval native_compute in let _ := Prop in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End T. + +Section U0. + Let n : unit := tt. + Eval native_compute in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. native_compute. Abort. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End U0. + +Section S0. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval native_compute in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. native_compute. Abort. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End S0. + +Class T := { }. +Section S1. + Context {p : T}. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval native_compute in _. +(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. native_compute. Abort. +(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *) +End S1. + +Class M := { m : Type }. +Section S2. + Context {p : M}. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval native_compute in _. +(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *) + Goal exists tt : unit, tt = tt. eexists. native_compute. Abort. +(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *) +End S2. diff --git a/test-suite/bugs/closed/8126.v b/test-suite/bugs/closed/8126.v new file mode 100644 index 0000000000..f52dfc6b47 --- /dev/null +++ b/test-suite/bugs/closed/8126.v @@ -0,0 +1,13 @@ +(* See also output test Notations4.v *) + +Inductive foo := tt. +Bind Scope foo_scope with foo. +Delimit Scope foo_scope with foo. +Notation "'HI'" := tt : foo_scope. +Definition myfoo (x : nat) (y : nat) (z : foo) := y. +Notation myfoo0 := (@myfoo 0). +Notation myfoo01 := (@myfoo0 1). +Check myfoo 0 1 HI. (* prints [myfoo0 1 HI], but should print [myfoo01 HI] *) +Check myfoo0 1 HI. (* prints [myfoo0 1 HI], but should print [myfoo01 HI] *) +Check myfoo01 tt. (* prints [myfoo0 1 HI], but should print [myfoo01 HI] *) +Check myfoo01 HI. (* was failing *) diff --git a/test-suite/bugs/closed/8215.v b/test-suite/bugs/closed/8215.v new file mode 100644 index 0000000000..c4b29a6354 --- /dev/null +++ b/test-suite/bugs/closed/8215.v @@ -0,0 +1,14 @@ +(* Check that instances for local definitions in evars have compatible body *) +Goal False. +Proof. + pose (n := 1). + evar (m:nat). + subst n. + pose (n := 0). + Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *) + clearbody n. + Fail Check ?m. (* n cannot be reinterpreted with a value convertible to 1 *) + clear n. + pose (n := 0+1). + Check ?m. (* Should be ok *) +Abort. diff --git a/test-suite/bugs/closed/8270.v b/test-suite/bugs/closed/8270.v new file mode 100644 index 0000000000..f36f757f10 --- /dev/null +++ b/test-suite/bugs/closed/8270.v @@ -0,0 +1,15 @@ +(* Don't do zeta in cbn when not asked for *) + +Goal let x := 0 in + let y := x in + y = 0. + (* We use "cofix" as an example because there are obviously no + cofixpoints in sight. This problem arises with any set of + reduction flags (not including zeta where the lets are of course reduced away) *) + cbn cofix. + intro x. + unfold x at 1. (* Should succeed *) + Undo 2. + cbn zeta. + Fail unfold x at 1. +Abort. diff --git a/test-suite/bugs/closed/8288.v b/test-suite/bugs/closed/8288.v new file mode 100644 index 0000000000..0350be9c06 --- /dev/null +++ b/test-suite/bugs/closed/8288.v @@ -0,0 +1,7 @@ +Set Universe Polymorphism. +Set Printing Universes. + +Set Polymorphic Inductive Cumulativity. + +Inductive foo := C : (forall A : Type -> Type, A Type) -> foo. +(* anomaly invalid subtyping relation *) diff --git a/test-suite/bugs/closed/8432.v b/test-suite/bugs/closed/8432.v new file mode 100644 index 0000000000..844ee12668 --- /dev/null +++ b/test-suite/bugs/closed/8432.v @@ -0,0 +1,39 @@ +Require Import Program.Tactics. + +Obligation Tactic := idtac. +Set Universe Polymorphism. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. + +Inductive Empty : Type :=. +Inductive Unit : Type := tt. +Definition not (A : Type) := A -> Empty. + + Lemma nat_path_O_S (n : nat) (H : paths O (S n)) : Empty. + Proof. refine ( + match H in paths _ i return + match i with + | O => Unit + | S _ => Empty + end + with + | idpath _ => tt + end + ). Defined. + Lemma symmetry {A} (x y : A) (p : paths x y) : paths y x. + Proof. + destruct p. apply idpath. + Defined. + Lemma nat_path_S_O (n : nat) (H : paths (S n) O) : Empty. + Proof. eapply nat_path_O_S. exact (symmetry _ _ H). Defined. +Set Printing Universes. +Program Fixpoint succ_not_zero (n:nat) : not (paths (S n) 0) := +match n as n return not (paths (S n) 0) with +| 0 => nat_path_S_O _ +| S n' => let dummy := succ_not_zero n' in _ +end. +Next Obligation. + intros f _ n dummy H. exact (nat_path_S_O _ H). + Show Universes. +Defined. diff --git a/test-suite/bugs/closed/8532.v b/test-suite/bugs/closed/8532.v new file mode 100644 index 0000000000..00aa66e701 --- /dev/null +++ b/test-suite/bugs/closed/8532.v @@ -0,0 +1,8 @@ +(* Checking Print Assumptions relatively to a bound module *) + +Module Type Typ. + Parameter Inline(10) t : Type. +End Typ. +Module Terms_mod (SetVars : Typ). +Print Assumptions SetVars.t. +End Terms_mod. |