diff options
Diffstat (limited to 'test-suite/bugs/opened')
-rw-r--r-- | test-suite/bugs/opened/2800.v | 6 | ||||
-rw-r--r-- | test-suite/bugs/opened/3383.v | 7 | ||||
-rw-r--r-- | test-suite/bugs/opened/3410.v | 1 | ||||
-rw-r--r-- | test-suite/bugs/opened/3753.v | 4 | ||||
-rw-r--r-- | test-suite/bugs/opened/3849.v | 8 | ||||
-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/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 | ||||
-rw-r--r-- | test-suite/bugs/opened/4214.v | 5 | ||||
-rw-r--r-- | test-suite/bugs/opened/4813.v | 5 |
17 files changed, 217 insertions, 31 deletions
diff --git a/test-suite/bugs/opened/2800.v b/test-suite/bugs/opened/2800.v deleted file mode 100644 index c559ab0c1..000000000 --- a/test-suite/bugs/opened/2800.v +++ /dev/null @@ -1,6 +0,0 @@ -Goal False. - -Fail intuition - match goal with - | |- _ => idtac " foo" - end. diff --git a/test-suite/bugs/opened/3383.v b/test-suite/bugs/opened/3383.v deleted file mode 100644 index 9a14641a5..000000000 --- a/test-suite/bugs/opened/3383.v +++ /dev/null @@ -1,7 +0,0 @@ -Goal forall b : bool, match b as b' return if b' then True else True with true => I | false => I end = match b as b' return if b' then True else True with true => I | false => I end. -intro. -Fail lazymatch goal with -| [ |- appcontext[match ?b as b' return @?P b' with true => ?t | false => ?f end] ] - => change (match b as b' return P b with true => t | false => f end) with (@bool_rect P t f) -end. (* Toplevel input, characters 153-154: -Error: The reference P was not found in the current environment. *) diff --git a/test-suite/bugs/opened/3410.v b/test-suite/bugs/opened/3410.v deleted file mode 100644 index 0d259181a..000000000 --- a/test-suite/bugs/opened/3410.v +++ /dev/null @@ -1 +0,0 @@ -Fail repeat match goal with H:_ |- _ => setoid_rewrite X in H end. diff --git a/test-suite/bugs/opened/3753.v b/test-suite/bugs/opened/3753.v deleted file mode 100644 index 05d77c831..000000000 --- a/test-suite/bugs/opened/3753.v +++ /dev/null @@ -1,4 +0,0 @@ -Axiom foo : Type -> Type. -Axiom bar : forall (T : Type), T -> foo T. -Arguments bar A x : rename. -Fail About bar. diff --git a/test-suite/bugs/opened/3849.v b/test-suite/bugs/opened/3849.v deleted file mode 100644 index 5290054a0..000000000 --- a/test-suite/bugs/opened/3849.v +++ /dev/null @@ -1,8 +0,0 @@ -Tactic Notation "foo" hyp_list(hs) := clear hs. - -Tactic Notation "bar" hyp_list(hs) := foo hs. - -Goal True. -do 5 pose proof 0 as ?n0. -foo n1 n2. -Fail bar n3 n4. 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/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 diff --git a/test-suite/bugs/opened/4214.v b/test-suite/bugs/opened/4214.v deleted file mode 100644 index 3daf45213..000000000 --- a/test-suite/bugs/opened/4214.v +++ /dev/null @@ -1,5 +0,0 @@ -(* Check that subst uses all equations around *) -Goal forall A (a b c : A), b = a -> b = c -> a = c. -intros. -subst. -Fail reflexivity. diff --git a/test-suite/bugs/opened/4813.v b/test-suite/bugs/opened/4813.v new file mode 100644 index 000000000..b75170179 --- /dev/null +++ b/test-suite/bugs/opened/4813.v @@ -0,0 +1,5 @@ +(* An example one would like to see succeeding *) + +Record T := BT { t : Set }. +Record U (x : T) := BU { u : t x -> Prop }. +Fail Definition A (H : unit -> Prop) : U (BT unit) := BU _ H. |