summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-08-20 18:27:01 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-08-20 18:27:01 +0200
commite0d682ec25282a348d35c5b169abafec48555690 (patch)
tree1a46f0142a85df553388c932110793881f3af52f /test-suite/bugs/closed/shouldsucceed
parent86535d84cc3cffeee1dcd8545343f234e7285530 (diff)
Imported Upstream version 8.4dfsgupstream/8.4dfsg
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1414.v4
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1784.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1844.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1935.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2127.v4
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2817.v9
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2836.v39
7 files changed, 55 insertions, 7 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v
index 495a16bc..ee9e2504 100644
--- a/test-suite/bugs/closed/shouldsucceed/1414.v
+++ b/test-suite/bugs/closed/shouldsucceed/1414.v
@@ -26,13 +26,13 @@ Program Fixpoint union
| t1,Leaf => t1
| Node l1 v1 r1 h1, Node l2 v2 r2 h2 =>
if (Z_ge_lt_dec h1 h2) then
- if (Z_eq_dec h2 1)
+ if (Z.eq_dec h2 1)
then add v2 s
else
let (l2', r2') := split v1 u in
join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _)
else
- if (Z_eq_dec h1 1)
+ if (Z.eq_dec h1 1)
then add v1 s
else
let (l1', r1') := split v2 u in
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index 718b0e86..fb2f0ca9 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -58,7 +58,7 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
match x with
| I x =>
match y with
- | I y => if (Z_eq_dec x y) then in_left else in_right
+ | I y => if (Z.eq_dec x y) then in_left else in_right
| S ys => in_right
end
| S xs =>
diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v
index 5627612f..17eeb352 100644
--- a/test-suite/bugs/closed/shouldsucceed/1844.v
+++ b/test-suite/bugs/closed/shouldsucceed/1844.v
@@ -1,6 +1,6 @@
Require Import ZArith.
-Definition zeq := Z_eq_dec.
+Definition zeq := Z.eq_dec.
Definition update (A: Set) (x: Z) (v: A) (s: Z -> A) : Z -> A :=
fun y => if zeq x y then v else s y.
diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v
index 72396d49..d5837619 100644
--- a/test-suite/bugs/closed/shouldsucceed/1935.v
+++ b/test-suite/bugs/closed/shouldsucceed/1935.v
@@ -13,7 +13,7 @@ Qed.
Require Import ZArith.
-Definition f'' (a:bool) := if a then eq (A:= Z) else Zlt.
+Definition f'' (a:bool) := if a then eq (A:= Z) else Z.lt.
Lemma f_refl'' : forall n , f'' true n n.
Proof.
diff --git a/test-suite/bugs/closed/shouldsucceed/2127.v b/test-suite/bugs/closed/shouldsucceed/2127.v
index 0fc854b6..142ada26 100644
--- a/test-suite/bugs/closed/shouldsucceed/2127.v
+++ b/test-suite/bugs/closed/shouldsucceed/2127.v
@@ -1,8 +1,8 @@
-(* Check that "apply refl_equal" is not exported as an interactive
+(* Check that "apply eq_refl" is not exported as an interactive
tactic but as a statically globalized one *)
(* (this is a simplification of the original bug report) *)
Module A.
-Hint Rewrite sym_equal using apply refl_equal : foo.
+Hint Rewrite eq_sym using apply eq_refl : foo.
End A.
diff --git a/test-suite/bugs/closed/shouldsucceed/2817.v b/test-suite/bugs/closed/shouldsucceed/2817.v
new file mode 100644
index 00000000..08dff992
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2817.v
@@ -0,0 +1,9 @@
+(** Occur-check for Meta (up to application of already known instances) *)
+
+Goal forall (f: nat -> nat -> Prop) (x:bool)
+ (H: forall (u: nat), f u u -> True)
+ (H0: forall x0, f (if x then x0 else x0) x0),
+False.
+
+intros.
+Fail apply H in H0. (* should fail without exhausting the stack *)
diff --git a/test-suite/bugs/closed/shouldsucceed/2836.v b/test-suite/bugs/closed/shouldsucceed/2836.v
new file mode 100644
index 00000000..a948b75e
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2836.v
@@ -0,0 +1,39 @@
+(* Check that possible instantiation made during evar materialization
+ are taken into account and do not raise Not_found *)
+
+Set Implicit Arguments.
+
+Record SpecializedCategory (obj : Type) (Morphism : obj -> obj -> Type) := {
+ Object :> _ := obj;
+
+ Identity' : forall o, Morphism o o;
+ Compose' : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+}.
+
+Section SpecializedCategoryInterface.
+ Variable obj : Type.
+ Variable mor : obj -> obj -> Type.
+ Variable C : @SpecializedCategory obj mor.
+
+ Definition Morphism (s d : C) := mor s d.
+ Definition Identity (o : C) : Morphism o o := C.(Identity') o.
+ Definition Compose (s d d' : C) (m : Morphism d d') (m0 : Morphism s d) :
+Morphism s d' := C.(Compose') s d d' m m0.
+End SpecializedCategoryInterface.
+
+Section ProductCategory.
+ Variable objC : Type.
+ Variable morC : objC -> objC -> Type.
+ Variable objD : Type.
+ Variable morD : objD -> objD -> Type.
+ Variable C : SpecializedCategory morC.
+ Variable D : SpecializedCategory morD.
+
+(* Should fail nicely *)
+Definition ProductCategory : @SpecializedCategory (objC * objD)%type (fun s d
+=> (morC (fst s) (fst d) * morD (snd s) (snd d))%type).
+Fail refine {|
+ Identity' := (fun o => (Identity (fst o), Identity (snd o)));
+ Compose' := (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd
+m2) (snd m1)))
+ |}.