diff options
Diffstat (limited to 'test-suite/bugs')
-rw-r--r-- | test-suite/bugs/closed/3911.v | 26 | ||||
-rw-r--r-- | test-suite/bugs/closed/3929.v | 12 | ||||
-rw-r--r-- | test-suite/bugs/closed/3957.v | 6 | ||||
-rw-r--r-- | test-suite/bugs/closed/4214.v (renamed from test-suite/bugs/opened/4214.v) | 3 | ||||
-rw-r--r-- | test-suite/bugs/opened/3889.v | 11 | ||||
-rw-r--r-- | test-suite/bugs/opened/3890.v | 18 | ||||
-rw-r--r-- | test-suite/bugs/opened/3916.v | 3 | ||||
-rw-r--r-- | test-suite/bugs/opened/3919.v-disabled | 13 | ||||
-rw-r--r-- | test-suite/bugs/opened/3922.v-disabled | 83 | ||||
-rw-r--r-- | test-suite/bugs/opened/3923.v | 33 | ||||
-rw-r--r-- | test-suite/bugs/opened/3926.v | 30 | ||||
-rw-r--r-- | test-suite/bugs/opened/3928.v-disabled | 12 | ||||
-rw-r--r-- | test-suite/bugs/opened/3938.v | 6 | ||||
-rw-r--r-- | test-suite/bugs/opened/3946.v | 11 | ||||
-rw-r--r-- | test-suite/bugs/opened/3948.v | 25 |
15 files changed, 291 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3911.v b/test-suite/bugs/closed/3911.v new file mode 100644 index 000000000..b289eafbf --- /dev/null +++ b/test-suite/bugs/closed/3911.v @@ -0,0 +1,26 @@ +(* Tested against coq ee596bc *) + +Set Nonrecursive Elimination Schemes. +Set Primitive Projections. +Set Universe Polymorphism. + +Record setoid := { base : Type }. + +Definition catdata (Obj Arr : Type) : Type := nat. + (* [nat] can be replaced by any other type, it seems, + without changing the error *) + +Record cat : Type := + { + obj : setoid; + arr : Type; + dta : catdata (base obj) arr + }. + +Definition bcwa (C:cat) (B:setoid) :Type := nat. + (* As above, nothing special about [nat] here. *) + +Record temp {C}{B} (e:bcwa C B) := + { fld : base (obj C) }. + +Print temp_rect. diff --git a/test-suite/bugs/closed/3929.v b/test-suite/bugs/closed/3929.v new file mode 100644 index 000000000..4031dcc45 --- /dev/null +++ b/test-suite/bugs/closed/3929.v @@ -0,0 +1,12 @@ +Goal True. +evar (T:Type). +pose (Z:=nat). +let Tv:=eval cbv [T] in T in +pose (x:=Tv). +revert x. +refine (_ : let x:=Z in True). +let Zv:=eval cbv [Z] in Z in +let Tv:=eval cbv [T] in T in +constr_eq Zv Tv. +Abort. + diff --git a/test-suite/bugs/closed/3957.v b/test-suite/bugs/closed/3957.v new file mode 100644 index 000000000..e20a6e97f --- /dev/null +++ b/test-suite/bugs/closed/3957.v @@ -0,0 +1,6 @@ +Ltac foo tac := tac. + +Goal True. +Proof. +foo subst. +Admitted. diff --git a/test-suite/bugs/opened/4214.v b/test-suite/bugs/closed/4214.v index 3daf45213..d684e8cf4 100644 --- a/test-suite/bugs/opened/4214.v +++ b/test-suite/bugs/closed/4214.v @@ -2,4 +2,5 @@ Goal forall A (a b c : A), b = a -> b = c -> a = c. intros. subst. -Fail reflexivity. +reflexivity. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/opened/3889.v b/test-suite/bugs/opened/3889.v new file mode 100644 index 000000000..6b287324c --- /dev/null +++ b/test-suite/bugs/opened/3889.v @@ -0,0 +1,11 @@ +Require Import Program. + +Inductive Even : nat -> Prop := +| evenO : Even O +| evenS : forall n, Odd n -> Even (S n) +with Odd : nat -> Prop := +| oddS : forall n, Even n -> Odd (S n). +Axiom admit : forall {T}, T. +Program Fixpoint doubleE {n} (e : Even n) : Even (2 * n) := admit +with doubleO {n} (o : Odd n) : Odd (S (2 * n)) := _. +Next Obligation of doubleE. diff --git a/test-suite/bugs/opened/3890.v b/test-suite/bugs/opened/3890.v new file mode 100644 index 000000000..f9ac9be2c --- /dev/null +++ b/test-suite/bugs/opened/3890.v @@ -0,0 +1,18 @@ +Class Foo. +Class Bar := b : Type. + +Instance foo : Foo := _. +(* 1 subgoals, subgoal 1 (ID 4) + + ============================ + Foo *) + +Instance bar : Bar. +exact Type. +Defined. +(* bar is defined *) + +About foo. +(* foo not a defined object. *) + +Fail Defined. diff --git a/test-suite/bugs/opened/3916.v b/test-suite/bugs/opened/3916.v new file mode 100644 index 000000000..fd95503e6 --- /dev/null +++ b/test-suite/bugs/opened/3916.v @@ -0,0 +1,3 @@ +Require Import List. + +Fail Hint Resolve -> in_map. (* Also happens when using <- instead of -> *) diff --git a/test-suite/bugs/opened/3919.v-disabled b/test-suite/bugs/opened/3919.v-disabled new file mode 100644 index 000000000..0d661de9c --- /dev/null +++ b/test-suite/bugs/opened/3919.v-disabled @@ -0,0 +1,13 @@ +Require Import MSets. +Require Import Orders. + +Declare Module Signal : OrderedType. + +Module S := MSetAVL.Make(Signal). +Module Sdec := Decide(S). +Export Sdec. + +Hint Extern 0 (Signal.eq ?x ?y) => now symmetry. + +Goal forall o s, Signal.eq o s. +Proof. fsetdec. Qed. diff --git a/test-suite/bugs/opened/3922.v-disabled b/test-suite/bugs/opened/3922.v-disabled new file mode 100644 index 000000000..ce4f509ca --- /dev/null +++ b/test-suite/bugs/opened/3922.v-disabled @@ -0,0 +1,83 @@ +Set Universe Polymorphism. +Notation Type0 := Set. + +Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. + +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. + +Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) + := forall x:A, f x = g x. + +Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope. + +Class Contr_internal (A : Type) := BuildContr { + center : A ; + contr : (forall y : A, center = y) +}. + +Inductive trunc_index : Type := +| minus_two : trunc_index +| trunc_S : trunc_index -> trunc_index. + +Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope. +Local Open Scope trunc_scope. +Notation "-2" := minus_two (at level 0) : trunc_scope. +Notation "-1" := (-2.+1) (at level 0) : trunc_scope. + +Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := + match n with + | -2 => Contr_internal A + | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y) + end. + +Class IsTrunc (n : trunc_index) (A : Type) : Type := + Trunc_is_trunc : IsTrunc_internal n A. + +Notation Contr := (IsTrunc -2). +Notation IsHProp := (IsTrunc -1). + +Monomorphic Axiom dummy_funext_type : Type0. +Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. + +Inductive Unit : Type1 := + tt : Unit. + +Record TruncType (n : trunc_index) := BuildTruncType { + trunctype_type : Type ; + istrunc_trunctype_type : IsTrunc n trunctype_type +}. + +Arguments BuildTruncType _ _ {_}. + +Coercion trunctype_type : TruncType >-> Sortclass. + +Notation "n -Type" := (TruncType n) (at level 1) : type_scope. +Notation hProp := (-1)-Type. + +Notation BuildhProp := (BuildTruncType -1). + +Private Inductive Trunc (n : trunc_index) (A :Type) : Type := + tr : A -> Trunc n A. +Arguments tr {n A} a. + +Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i}) +: IsTrunc@{j} n (Trunc@{i} n A). +Admitted. + +Definition Trunc_ind {n A} + (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)} + : (forall a, P (tr a)) -> (forall aa, P aa) +:= (fun f aa => match aa with tr a => fun _ => f a end Pt). +Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A). +Definition cconst_factors_contr `{Funext} {X Y : Type} (f : X -> Y) + (P : Type) `{Pc : X -> Contr P} + (g : X -> P) (h : P -> Y) (p : h o g == f) +: Unit. +Proof. + assert (merely X -> IsHProp P) by admit. + refine (let g' := Trunc_ind (fun _ => P) g : merely X -> P in _); + [ assumption.. | ]. + Fail pose (g' := Trunc_ind (fun _ => P) g : merely X -> P). diff --git a/test-suite/bugs/opened/3923.v b/test-suite/bugs/opened/3923.v new file mode 100644 index 000000000..6aa6b4932 --- /dev/null +++ b/test-suite/bugs/opened/3923.v @@ -0,0 +1,33 @@ +Module Type TRIVIAL. +Parameter t:Type. +End TRIVIAL. + +Module MkStore (Key : TRIVIAL). + +Module St : TRIVIAL. +Definition t := unit. +End St. + +End MkStore. + + + +Module Type CERTRUNTIMETYPES (B : TRIVIAL). + +Parameter cert_fieldstore : Type. +Parameter empty_fieldstore : cert_fieldstore. + +End CERTRUNTIMETYPES. + + + +Module MkCertRuntimeTypes (B : TRIVIAL) : CERTRUNTIMETYPES B. + +Module FieldStore := MkStore B. + +Definition cert_fieldstore := FieldStore.St.t. +Axiom empty_fieldstore : cert_fieldstore. + +End MkCertRuntimeTypes. + +Fail Extraction MkCertRuntimeTypes. diff --git a/test-suite/bugs/opened/3926.v b/test-suite/bugs/opened/3926.v new file mode 100644 index 000000000..cfad76357 --- /dev/null +++ b/test-suite/bugs/opened/3926.v @@ -0,0 +1,30 @@ +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/3928.v-disabled b/test-suite/bugs/opened/3928.v-disabled new file mode 100644 index 000000000..b470eb229 --- /dev/null +++ b/test-suite/bugs/opened/3928.v-disabled @@ -0,0 +1,12 @@ +Typeclasses eauto := bfs. + +Class Foo := {}. +Class Bar := {}. + +Instance: Bar. +Instance: Foo -> Bar -> Foo -> Foo | 1. +Instance: Bar -> Foo | 100. +Instance: Foo -> Bar -> Foo -> Foo | 1. + +Set Typeclasses Debug. +Timeout 1 Check (_ : Foo). (* timeout *) diff --git a/test-suite/bugs/opened/3938.v b/test-suite/bugs/opened/3938.v new file mode 100644 index 000000000..2d0d1930f --- /dev/null +++ b/test-suite/bugs/opened/3938.v @@ -0,0 +1,6 @@ +Require Import Coq.Arith.PeanoNat. +Hint Extern 1 => admit : typeclass_instances. +Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b. + intros a b f H. + rewrite H. (* Toplevel input, characters 15-25: +Anomaly: Evar ?X11 was not declared. Please report. *) diff --git a/test-suite/bugs/opened/3946.v b/test-suite/bugs/opened/3946.v new file mode 100644 index 000000000..e77bdbc65 --- /dev/null +++ b/test-suite/bugs/opened/3946.v @@ -0,0 +1,11 @@ +Require Import ZArith. + +Inductive foo := Foo : Z.le 0 1 -> foo. + +Definition bar (f : foo) := let (f) := f in f. + +(* Doesn't work: *) +(* Arguments bar f.*) + +(* Does work *) +Arguments bar f _. diff --git a/test-suite/bugs/opened/3948.v b/test-suite/bugs/opened/3948.v new file mode 100644 index 000000000..165813084 --- /dev/null +++ b/test-suite/bugs/opened/3948.v @@ -0,0 +1,25 @@ +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.
\ No newline at end of file |