summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1100.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1322.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1411.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1414.v41
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1416.v27
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1425.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1446.v8
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1507.v14
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1568.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1576.v6
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1582.v6
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1618.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1634.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1643.v1
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1683.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1711.v34
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1738.v6
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1740.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1775.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1776.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1784.v14
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1791.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1844.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1891.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1901.v6
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1905.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1918.v39
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1925.v10
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1931.v4
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1935.v4
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1939.v19
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1944.v9
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1951.v63
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1981.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2001.v10
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2017.v6
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2083.v27
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2095.v19
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2108.v22
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2117.v56
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2123.v11
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2127.v11
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2135.v9
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2136.v61
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2137.v52
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2139.v24
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2145.v20
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2193.v31
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2231.v3
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2244.v19
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2255.v21
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2281.v50
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2295.v11
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2299.v13
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2300.v15
-rw-r--r--test-suite/bugs/closed/shouldsucceed/335.v5
-rw-r--r--test-suite/bugs/closed/shouldsucceed/38.v2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/846.v10
58 files changed, 741 insertions, 110 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1100.v b/test-suite/bugs/closed/shouldsucceed/1100.v
index 6d619c74..32c78b4b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1100.v
+++ b/test-suite/bugs/closed/shouldsucceed/1100.v
@@ -6,7 +6,7 @@ Parameter PQ : forall n, P n <-> Q n.
Lemma PQ2 : forall n, P n -> Q n.
intros.
- rewrite PQ in H.
+ rewrite PQ in H.
trivial.
Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1322.v b/test-suite/bugs/closed/shouldsucceed/1322.v
index 7e21aa7c..1ec7d452 100644
--- a/test-suite/bugs/closed/shouldsucceed/1322.v
+++ b/test-suite/bugs/closed/shouldsucceed/1322.v
@@ -7,7 +7,7 @@ Variable I_eq :I -> I -> Prop.
Variable I_eq_equiv : Setoid_Theory I I_eq.
(* Add Relation I I_eq
- reflexivity proved by I_eq_equiv.(Seq_refl I I_eq)
+ reflexivity proved by I_eq_equiv.(Seq_refl I I_eq)
symmetry proved by I_eq_equiv.(Seq_sym I I_eq)
transitivity proved by I_eq_equiv.(Seq_trans I I_eq)
as I_eq_relation. *)
diff --git a/test-suite/bugs/closed/shouldsucceed/1411.v b/test-suite/bugs/closed/shouldsucceed/1411.v
index e330d46f..a1a7b288 100644
--- a/test-suite/bugs/closed/shouldsucceed/1411.v
+++ b/test-suite/bugs/closed/shouldsucceed/1411.v
@@ -23,7 +23,7 @@ Program Fixpoint fetch t p (x:Exact t p) {struct t} :=
match t, p with
| No p' , nil => p'
| No p' , _::_ => unreachable nat _
- | Br l r, nil => unreachable nat _
+ | Br l r, nil => unreachable nat _
| Br l r, true::t => fetch l t _
| Br l r, false::t => fetch r t _
end.
diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v
index d3c00808..495a16bc 100644
--- a/test-suite/bugs/closed/shouldsucceed/1414.v
+++ b/test-suite/bugs/closed/shouldsucceed/1414.v
@@ -7,8 +7,8 @@ Inductive t : Set :=
| Node : t -> data -> t -> Z -> t.
Parameter avl : t -> Prop.
-Parameter bst : t -> Prop.
-Parameter In : data -> t -> Prop.
+Parameter bst : t -> Prop.
+Parameter In : data -> t -> Prop.
Parameter cardinal : t -> nat.
Definition card2 (s:t*t) := let (s1,s2) := s in cardinal s1 + cardinal s2.
@@ -16,26 +16,25 @@ Parameter split : data -> t -> t*(bool*t).
Parameter join : t -> data -> t -> t.
Parameter add : data -> t -> t.
-Program Fixpoint union
- (s:t*t)
- (hb1: bst (fst s))(ha1: avl (fst s))(hb2: bst (snd s))(hb2: avl (snd s))
- { measure card2 s } :
- {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x (fst s) \/ In x (snd
-s)} :=
- match s with
- | (Leaf,t2) => t2
- | (t1,Leaf) => t1
- | (Node l1 v1 r1 h1, Node l2 v2 r2 h2) =>
+Program Fixpoint union
+ (s u:t)
+ (hb1: bst s)(ha1: avl s)(hb2: bst u)(hb2: avl u)
+ { measure (cardinal s + cardinal u) } :
+ {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x s \/ In x u} :=
+ match s, u with
+ | Leaf,t2 => t2
+ | 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)
- then add v2 (fst s)
+ if (Z_eq_dec h2 1)
+ then add v2 s
else
- let (l2', r2') := split v1 (snd s) in
- join (union (l1,l2') _ _ _ _) v1 (union (r1,snd r2') _ _ _ _)
+ let (l2', r2') := split v1 u in
+ join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _)
else
- if (Z_eq_dec h1 1)
- then add v1 (snd s)
+ if (Z_eq_dec h1 1)
+ then add v1 s
else
- let (l1', r1') := split v2 (fst s) in
- join (union (l1',l2) _ _ _ _) v2 (union (snd r1',r2) _ _ _ _)
- end.
+ let (l1', r1') := split v2 u in
+ join (union l1' l2 _ _ _ _) v2 (union (snd r1') r2 _ _ _ _)
+ end.
diff --git a/test-suite/bugs/closed/shouldsucceed/1416.v b/test-suite/bugs/closed/shouldsucceed/1416.v
new file mode 100644
index 00000000..da67d9b0
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1416.v
@@ -0,0 +1,27 @@
+Set Implicit Arguments.
+
+Record Place (Env A: Type) : Type := {
+ read: Env -> A ;
+ write: Env -> A -> Env ;
+ write_read: forall (e:Env), (write e (read e))=e
+}.
+
+Hint Rewrite -> write_read: placeeq.
+
+Record sumPl (Env A B: Type) (vL:(Place Env A)) (vR:(Place Env B)) : Type :=
+ {
+ mkEnv: A -> B -> Env ;
+ mkEnv2writeL: forall (e:Env) (x:A), (mkEnv x (read vR e))=(write vL e x)
+ }.
+
+(* when the following line is commented, the bug does not appear *)
+Hint Rewrite -> mkEnv2writeL: placeeq.
+
+Lemma autorewrite_raise_anomaly: forall (Env A:Type) (e: Env) (p:Place Env A),
+ (exists e1:Env, e=(write p e1 (read p e))).
+Proof.
+ intros Env A e p; eapply ex_intro.
+ autorewrite with placeeq. (* Here is the bug *)
+ auto.
+Qed.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1425.v b/test-suite/bugs/closed/shouldsucceed/1425.v
index 8e26209a..6be30174 100644
--- a/test-suite/bugs/closed/shouldsucceed/1425.v
+++ b/test-suite/bugs/closed/shouldsucceed/1425.v
@@ -1,4 +1,4 @@
-Require Import Setoid.
+Require Import Setoid.
Parameter recursion : forall A : Set, A -> (nat -> A -> A) -> nat -> A.
diff --git a/test-suite/bugs/closed/shouldsucceed/1446.v b/test-suite/bugs/closed/shouldsucceed/1446.v
index d4e7cea8..8cb2d653 100644
--- a/test-suite/bugs/closed/shouldsucceed/1446.v
+++ b/test-suite/bugs/closed/shouldsucceed/1446.v
@@ -1,8 +1,8 @@
Lemma not_true_eq_false : forall (b:bool), b <> true -> b = false.
Proof.
- destruct b;intros;trivial.
- elim H.
- exact (refl_equal true).
+ destruct b;intros;trivial.
+ elim H.
+ exact (refl_equal true).
Qed.
Section BUG.
@@ -13,7 +13,7 @@ Section BUG.
Hypothesis H1 : b <> true.
Goal False.
- rewrite (not_true_eq_false _ H) in * |-.
+ rewrite (not_true_eq_false _ H) in * |-.
contradiction.
Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v
index b484c7dc..f1872a2b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1507.v
+++ b/test-suite/bugs/closed/shouldsucceed/1507.v
@@ -2,16 +2,16 @@
Implementing reals a la Stolzenberg
Danko Ilik, March 2007
- svn revision: $Id: 1507.v 10068 2007-08-10 12:06:59Z notin $
+ svn revision: $Id$
XField.v -- (unfinished) axiomatisation of the theories of real and
rational intervals.
*)
-Definition associative (A:Type)(op:A->A->A) :=
+Definition associative (A:Type)(op:A->A->A) :=
forall x y z:A, op (op x y) z = op x (op y z).
-Definition commutative (A:Type)(op:A->A->A) :=
+Definition commutative (A:Type)(op:A->A->A) :=
forall x y:A, op x y = op y x.
Definition trichotomous (A:Type)(R:A->A->Prop) :=
@@ -19,7 +19,7 @@ Definition trichotomous (A:Type)(R:A->A->Prop) :=
Definition relation (A:Type) := A -> A -> Prop.
Definition reflexive (A:Type)(R:relation A) := forall x:A, R x x.
-Definition transitive (A:Type)(R:relation A) :=
+Definition transitive (A:Type)(R:relation A) :=
forall x y z:A, R x y -> R y z -> R x z.
Definition symmetric (A:Type)(R:relation A) := forall x y:A, R x y -> R y x.
@@ -52,7 +52,7 @@ Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake {
Iplus_opp_r : forall x:Icar, Ic (Iplus x (Iopp x)) (Izero);
Imult_inv_r : forall x:Icar, ~(Ic x Izero) -> Ic (Imult x (Iinv x)) Ione;
(* distributive laws *)
- Imult_plus_distr_l : forall x x' y y' z z' z'',
+ Imult_plus_distr_l : forall x x' y y' z z' z'',
Ic x x' -> Ic y y' -> Ic z z' -> Ic z z'' ->
Ic (Imult (Iplus x y) z) (Iplus (Imult x' z') (Imult y' z''));
(* order and lattice structure *)
@@ -70,7 +70,7 @@ Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake {
Ic_sym : symmetric _ Ic
}.
-Definition interval_set (X:Set)(le:X->X->Prop) :=
+Definition interval_set (X:Set)(le:X->X->Prop) :=
(interval X le) -> Prop. (* can be Set as well *)
Check interval_set.
Check Ic.
@@ -101,7 +101,7 @@ Record N (grnd:Set)(le:grnd->grnd->Prop)(grndI:I grnd le) : Type := Nmake {
Nplus_opp_r : forall x:Ncar, Nc (Nplus x (Nopp x)) (Nzero);
Nmult_inv_r : forall x:Ncar, ~(Nc x Nzero) -> Nc (Nmult x (Ninv x)) None;
(* distributive laws *)
- Nmult_plus_distr_l : forall x x' y y' z z' z'',
+ Nmult_plus_distr_l : forall x x' y y' z z' z'',
Nc x x' -> Nc y y' -> Nc z z' -> Nc z z'' ->
Nc (Nmult (Nplus x y) z) (Nplus (Nmult x' z') (Nmult y' z''));
(* order and lattice structure *)
diff --git a/test-suite/bugs/closed/shouldsucceed/1568.v b/test-suite/bugs/closed/shouldsucceed/1568.v
index 9f10f749..3609e9c8 100644
--- a/test-suite/bugs/closed/shouldsucceed/1568.v
+++ b/test-suite/bugs/closed/shouldsucceed/1568.v
@@ -3,7 +3,7 @@ CoInductive A: Set :=
with B: Set :=
mk_B: A -> B.
-CoFixpoint a:A := mk_A b
+CoFixpoint a:A := mk_A b
with b:B := mk_B a.
Goal b = match a with mk_A a1 => a1 end.
diff --git a/test-suite/bugs/closed/shouldsucceed/1576.v b/test-suite/bugs/closed/shouldsucceed/1576.v
index c9ebbd14..3621f7a1 100644
--- a/test-suite/bugs/closed/shouldsucceed/1576.v
+++ b/test-suite/bugs/closed/shouldsucceed/1576.v
@@ -13,8 +13,8 @@ End TC.
Module Type TD.
Declare Module B: TB .
-Declare Module C: TC
- with Module B := B .
+Declare Module C: TC
+ with Module B := B .
End TD.
Module Type TE.
@@ -25,7 +25,7 @@ Module Type TF.
Declare Module E: TE.
End TF.
-Module G (D: TD).
+Module G (D: TD).
Module B' := D.C.B.
End G.
diff --git a/test-suite/bugs/closed/shouldsucceed/1582.v b/test-suite/bugs/closed/shouldsucceed/1582.v
index 47953a66..be5d3dd2 100644
--- a/test-suite/bugs/closed/shouldsucceed/1582.v
+++ b/test-suite/bugs/closed/shouldsucceed/1582.v
@@ -1,12 +1,12 @@
Require Import Peano_dec.
-Definition fact_F :
+Definition fact_F :
forall (n:nat),
(forall m, m<n -> nat) ->
nat.
-refine
+refine
(fun n fact_rec =>
- if eq_nat_dec n 0 then
+ if eq_nat_dec n 0 then
1
else
let fn := fact_rec (n-1) _ in
diff --git a/test-suite/bugs/closed/shouldsucceed/1618.v b/test-suite/bugs/closed/shouldsucceed/1618.v
index a90290bf..a9b067ce 100644
--- a/test-suite/bugs/closed/shouldsucceed/1618.v
+++ b/test-suite/bugs/closed/shouldsucceed/1618.v
@@ -6,7 +6,7 @@ Definition A_size (a: A) : nat :=
| A1 n => 0
end.
-Require Import Recdef.
+Require Import Recdef.
Function n3 (P: A -> Prop) (f: forall n, P (A1 n)) (a: A) {struct a} : P a :=
match a return (P a) with
diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/shouldsucceed/1634.v
index e0c540f3..0150c250 100644
--- a/test-suite/bugs/closed/shouldsucceed/1634.v
+++ b/test-suite/bugs/closed/shouldsucceed/1634.v
@@ -18,7 +18,7 @@ Add Parametric Relation a : (S a) Seq
Goal forall (a : A) (x y : S a), Seq x y -> Seq x y.
intros a x y H.
- setoid_replace x with y.
+ setoid_replace x with y.
reflexivity.
trivial.
Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1643.v b/test-suite/bugs/closed/shouldsucceed/1643.v
index 4114987d..879a65b1 100644
--- a/test-suite/bugs/closed/shouldsucceed/1643.v
+++ b/test-suite/bugs/closed/shouldsucceed/1643.v
@@ -10,7 +10,6 @@ Definition decomp_func (s:Str) :=
Theorem decomp s: s = decomp_func s.
Proof.
- intros s.
case s; simpl; reflexivity.
Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1683.v b/test-suite/bugs/closed/shouldsucceed/1683.v
index 1571ee20..3e99694b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1683.v
+++ b/test-suite/bugs/closed/shouldsucceed/1683.v
@@ -30,7 +30,7 @@ Add Parametric Relation A : (ms_type A) (ms_eq A)
Hypothesis foobar : forall n, ms_eq CR (IRasCR (foo IR n)) (foo CRasCRing n).
Goal forall (b:ms_type CR),
- ms_eq CR (IRasCR (foo IR O)) b ->
+ ms_eq CR (IRasCR (foo IR O)) b ->
ms_eq CR (IRasCR (foo IR O)) b.
intros b H.
rewrite foobar.
diff --git a/test-suite/bugs/closed/shouldsucceed/1711.v b/test-suite/bugs/closed/shouldsucceed/1711.v
new file mode 100644
index 00000000..e16612e3
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1711.v
@@ -0,0 +1,34 @@
+(* Test for evar map consistency - was failing at some point and was *)
+(* assumed to be solved from revision 10151 (but using a bad fix) *)
+
+Require Import List.
+Set Implicit Arguments.
+
+Inductive rose : Set := Rose : nat -> list rose -> rose.
+
+Section RoseRec.
+Variables (P: rose -> Set)(L: list rose -> Set).
+Hypothesis
+ (R: forall n rs, L rs -> P (Rose n rs))
+ (Lnil: L nil)
+ (Lcons: forall r rs, P r -> L rs -> L (cons r rs)).
+
+Fixpoint rose_rec2 (t:rose) {struct t} : P t :=
+ match t as x return P x with
+ | Rose n rs =>
+ R n ((fix rs_ind (l' : list rose): L l' :=
+ match l' as x return L x with
+ | nil => Lnil
+ | cons t tl => Lcons (rose_rec2 t) (rs_ind tl)
+ end)
+ rs)
+ end.
+End RoseRec.
+
+Lemma rose_map : rose -> rose.
+Proof. intro H; elim H using rose_rec2 with
+ (L:=fun _ => list rose); (* was assumed to fail here *)
+(* (L:=fun (_:list rose) => list rose); *)
+ clear H; simpl; intros.
+ exact (Rose n rs). exact nil. exact (H::H0).
+Defined.
diff --git a/test-suite/bugs/closed/shouldsucceed/1738.v b/test-suite/bugs/closed/shouldsucceed/1738.v
index 0deed366..c2926a2b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1738.v
+++ b/test-suite/bugs/closed/shouldsucceed/1738.v
@@ -5,10 +5,10 @@ Module SomeSetoids (Import M:FSetInterface.S).
Lemma Equal_refl : forall s, s[=]s.
Proof. red; split; auto. Qed.
-Add Relation t Equal
- reflexivity proved by Equal_refl
+Add Relation t Equal
+ reflexivity proved by Equal_refl
symmetry proved by eq_sym
- transitivity proved by eq_trans
+ transitivity proved by eq_trans
as EqualSetoid.
Add Morphism Empty with signature Equal ==> iff as Empty_m.
diff --git a/test-suite/bugs/closed/shouldsucceed/1740.v b/test-suite/bugs/closed/shouldsucceed/1740.v
index d9ce546a..ec4a7a6b 100644
--- a/test-suite/bugs/closed/shouldsucceed/1740.v
+++ b/test-suite/bugs/closed/shouldsucceed/1740.v
@@ -17,7 +17,7 @@ Goal f =
| n, O => n
| _, _ => O
end.
- unfold f.
+ unfold f.
reflexivity.
Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1775.v b/test-suite/bugs/closed/shouldsucceed/1775.v
index dab4120b..932949a3 100644
--- a/test-suite/bugs/closed/shouldsucceed/1775.v
+++ b/test-suite/bugs/closed/shouldsucceed/1775.v
@@ -13,7 +13,7 @@ Goal forall s k k' m,
(pl k' (nexists (fun w => (nexists (fun b => pl (pair w w)
(pl (pair s b)
(nexists (fun w0 => (nexists (fun a => pl (pair b w0)
- (nexists (fun w1 => (nexists (fun c => pl
+ (nexists (fun w1 => (nexists (fun c => pl
(pair a w1) (pl (pair a c) k))))))))))))))) m.
intros.
eapply plImp; [ | eauto | intros ].
diff --git a/test-suite/bugs/closed/shouldsucceed/1776.v b/test-suite/bugs/closed/shouldsucceed/1776.v
index abf85455..58491f9d 100644
--- a/test-suite/bugs/closed/shouldsucceed/1776.v
+++ b/test-suite/bugs/closed/shouldsucceed/1776.v
@@ -10,7 +10,7 @@ Definition nexists (P:nat -> nat -> Prop) : nat -> Prop :=
Goal forall a A m,
True ->
- (pl A (nexists (fun x => (nexists
+ (pl A (nexists (fun x => (nexists
(fun y => pl (pair a (S x)) (pair a (S y))))))) m.
Proof.
intros.
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index 5855b168..718b0e86 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -56,16 +56,16 @@ Require Import Program.
Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
match x with
- | I x =>
+ | I x =>
match y with
| I y => if (Z_eq_dec x y) then in_left else in_right
| S ys => in_right
end
- | S xs =>
+ | S xs =>
match y with
| I y => in_right
| S ys =>
- let fix list_in (xs ys:list sv) {struct xs} :
+ let fix list_in (xs ys:list sv) {struct xs} :
{slist_in xs ys} + {~slist_in xs ys} :=
match xs with
| nil => in_left
@@ -76,8 +76,8 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
| y::ys => if lt_dec x y then in_left else if elem_in
ys then in_left else in_right
end
- in
- if elem_in ys then
+ in
+ if elem_in ys then
if list_in xs ys then in_left else in_right
else in_right
end
@@ -90,12 +90,12 @@ Next Obligation. intro H; inversion H. Defined.
Next Obligation. intro H; inversion H. Defined.
Next Obligation. intro H; inversion H; subst. Defined.
Next Obligation.
- intro H1; contradict H. inversion H1; subst. assumption.
+ intro H1; contradict H. inversion H1; subst. assumption.
contradict H0; assumption. Defined.
Next Obligation.
intro H1; contradict H0. inversion H1; subst. assumption. Defined.
Next Obligation.
- intro H0; contradict H. inversion H0; subst. assumption. Defined.
+ intro H1; contradict H. inversion H1; subst. assumption. Defined.
Next Obligation.
intro H0; contradict H. inversion H0; subst; auto. Defined.
diff --git a/test-suite/bugs/closed/shouldsucceed/1791.v b/test-suite/bugs/closed/shouldsucceed/1791.v
index 694f056e..be0e8ae8 100644
--- a/test-suite/bugs/closed/shouldsucceed/1791.v
+++ b/test-suite/bugs/closed/shouldsucceed/1791.v
@@ -9,7 +9,7 @@ Definition k1 := k0 -> k0.
(** iterating X n times *)
Fixpoint Pow (X:k1)(k:nat){struct k}:k1:=
match k with 0 => fun X => X
- | S k' => fun A => X (Pow X k' A)
+ | S k' => fun A => X (Pow X k' A)
end.
Parameter Bush: k1.
diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v
index 545f2615..5627612f 100644
--- a/test-suite/bugs/closed/shouldsucceed/1844.v
+++ b/test-suite/bugs/closed/shouldsucceed/1844.v
@@ -188,7 +188,7 @@ with exec_finish: function -> outcome -> store -> value -> store -> Prop :=
with exec_function: function -> store -> value -> store -> Prop :=
| exec_function_intro: forall f st out st1 v st',
- exec f.(fn_body) st out st1 ->
+ exec f.(fn_body) st out st1 ->
exec_finish f out st1 v st' ->
exec_function f st v st'.
diff --git a/test-suite/bugs/closed/shouldsucceed/1891.v b/test-suite/bugs/closed/shouldsucceed/1891.v
index 11124cdd..2d90a2f1 100644
--- a/test-suite/bugs/closed/shouldsucceed/1891.v
+++ b/test-suite/bugs/closed/shouldsucceed/1891.v
@@ -7,7 +7,7 @@
Lemma L (x: T unit): (unit -> T unit) -> unit.
Proof.
- refine (fun x => match x return _ with mkT n => fun g => f (g _) end).
+ refine (match x return _ with mkT n => fun g => f (g _) end).
trivial.
Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1901.v b/test-suite/bugs/closed/shouldsucceed/1901.v
index 598db366..7d86adbf 100644
--- a/test-suite/bugs/closed/shouldsucceed/1901.v
+++ b/test-suite/bugs/closed/shouldsucceed/1901.v
@@ -2,9 +2,9 @@ Require Import Relations.
Record Poset{A:Type}(Le : relation A) : Type :=
Build_Poset
- {
- Le_refl : forall x : A, Le x x;
- Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z;
+ {
+ Le_refl : forall x : A, Le x x;
+ Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z;
Le_antisym : forall x y : A, Le x y -> Le y x -> x = y }.
Definition nat_Poset : Poset Peano.le.
diff --git a/test-suite/bugs/closed/shouldsucceed/1905.v b/test-suite/bugs/closed/shouldsucceed/1905.v
index fb2725c9..8c81d751 100644
--- a/test-suite/bugs/closed/shouldsucceed/1905.v
+++ b/test-suite/bugs/closed/shouldsucceed/1905.v
@@ -5,7 +5,7 @@ Axiom t : Set.
Axiom In : nat -> t -> Prop.
Axiom InE : forall (x : nat) (s:t), impl (In x s) True.
-Goal forall a s,
+Goal forall a s,
In a s -> False.
Proof.
intros a s Ia.
diff --git a/test-suite/bugs/closed/shouldsucceed/1918.v b/test-suite/bugs/closed/shouldsucceed/1918.v
index 9d4a3e04..9d92fe12 100644
--- a/test-suite/bugs/closed/shouldsucceed/1918.v
+++ b/test-suite/bugs/closed/shouldsucceed/1918.v
@@ -35,7 +35,7 @@ Definition mon (X:k1) : Type := forall (A B:Set), (A -> B) -> X A -> X B.
(** extensionality *)
Definition ext (X:k1)(h: mon X): Prop :=
- forall (A B:Set)(f g:A -> B),
+ forall (A B:Set)(f g:A -> B),
(forall a, f a = g a) -> forall r, h _ _ f r = h _ _ g r.
(** first functor law *)
@@ -44,7 +44,7 @@ Definition fct1 (X:k1)(m: mon X) : Prop :=
(** second functor law *)
Definition fct2 (X:k1)(m: mon X) : Prop :=
- forall (A B C:Set)(f:A -> B)(g:B -> C)(x:X A),
+ forall (A B C:Set)(f:A -> B)(g:B -> C)(x:X A),
m _ _ (g o f) x = m _ _ g (m _ _ f x).
(** pack up the good properties of the approximation into
@@ -60,20 +60,20 @@ Definition pEFct (F:k2) : Type :=
forall (X:k1), EFct X -> EFct (F X).
-(** we show some closure properties of pEFct, depending on such properties
+(** we show some closure properties of pEFct, depending on such properties
for EFct *)
Definition moncomp (X Y:k1)(mX:mon X)(mY:mon Y): mon (fun A => X(Y A)).
Proof.
red.
- intros X Y mX mY A B f x.
+ intros A B f x.
exact (mX (Y A)(Y B) (mY A B f) x).
Defined.
(** closure under composition *)
Lemma compEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X(Y A)).
Proof.
- intros X Y ef1 ef2.
+ intros ef1 ef2.
apply (mkEFct(m:=moncomp (m ef1) (m ef2))); red; intros; unfold moncomp.
(* prove ext *)
apply (e ef1).
@@ -92,7 +92,7 @@ Proof.
apply (f2 ef2).
Defined.
-Corollary comppEFct (F G:k2): pEFct F -> pEFct G ->
+Corollary comppEFct (F G:k2): pEFct F -> pEFct G ->
pEFct (fun X A => F X (G X A)).
Proof.
red.
@@ -103,8 +103,8 @@ Defined.
(** closure under sums *)
Lemma sumEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A + Y A)%type.
Proof.
- intros X Y ef1 ef2.
- set (m12:=fun (A B:Set)(f:A->B) x => match x with
+ intros ef1 ef2.
+ set (m12:=fun (A B:Set)(f:A->B) x => match x with
| inl y => inl _ (m ef1 f y)
| inr y => inr _ (m ef2 f y)
end).
@@ -133,7 +133,7 @@ Proof.
rewrite (f2 ef2); reflexivity.
Defined.
-Corollary sumpEFct (F G:k2): pEFct F -> pEFct G ->
+Corollary sumpEFct (F G:k2): pEFct F -> pEFct G ->
pEFct (fun X A => F X A + G X A)%type.
Proof.
red.
@@ -144,8 +144,8 @@ Defined.
(** closure under products *)
Lemma prodEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A * Y A)%type.
Proof.
- intros X Y ef1 ef2.
- set (m12:=fun (A B:Set)(f:A->B) x => match x with
+ intros ef1 ef2.
+ set (m12:=fun (A B:Set)(f:A->B) x => match x with
(x1,x2) => (m ef1 f x1, m ef2 f x2) end).
apply (mkEFct(m:=m12)); red; intros.
(* prove ext *)
@@ -168,7 +168,7 @@ Proof.
apply (f2 ef2).
Defined.
-Corollary prodpEFct (F G:k2): pEFct F -> pEFct G ->
+Corollary prodpEFct (F G:k2): pEFct F -> pEFct G ->
pEFct (fun X A => F X A * G X A)%type.
Proof.
red.
@@ -220,7 +220,6 @@ Defined.
(** constants in k1 *)
Lemma constEFct (C:Set): EFct (fun _ => C).
Proof.
- intro.
set (mC:=fun A B (f:A->B)(x:C) => x).
apply (mkEFct(m:=mC)); red; intros; unfold mC; reflexivity.
Defined.
@@ -248,19 +247,19 @@ Module Type LNMIt_Type.
Parameter F:k2.
Parameter FpEFct: pEFct F.
-Parameter mu20: k1.
+Parameter mu20: k1.
Definition mu2: k1:= fun A => mu20 A.
Parameter mapmu2: mon mu2.
Definition MItType: Type :=
forall G : k1, (forall X : k1, X c_k1 G -> F X c_k1 G) -> mu2 c_k1 G.
Parameter MIt0 : MItType.
-Definition MIt : MItType:= fun G s A t => MIt0 s t.
-Definition InType : Type :=
- forall (X:k1)(ef:EFct X)(j: X c_k1 mu2),
+Definition MIt : MItType:= fun G s A t => MIt0 s t.
+Definition InType : Type :=
+ forall (X:k1)(ef:EFct X)(j: X c_k1 mu2),
NAT j (m ef) mapmu2 -> F X c_k1 mu2.
Parameter In : InType.
Axiom mapmu2Red : forall (A:Set)(X:k1)(ef:EFct X)(j: X c_k1 mu2)
- (n: NAT j (m ef) mapmu2)(t: F X A)(B:Set)(f:A->B),
+ (n: NAT j (m ef) mapmu2)(t: F X A)(B:Set)(f:A->B),
mapmu2 f (In ef n t) = In ef n (m (FpEFct ef) f t).
Axiom MItRed : forall (G : k1)
(s : forall X : k1, X c_k1 G -> F X c_k1 G)(X : k1)(ef:EFct X)(j: X c_k1 mu2)
@@ -327,8 +326,8 @@ Fixpoint Pow (X:k1)(k:nat){struct k}:k1:=
Fixpoint POW (k:nat)(X:k1)(m:mon X){struct k} : mon (Pow X k) :=
match k return mon (Pow X k)
- with 0 => fun _ _ f => f
- | S k' => fun _ _ f => m _ _ (POW k' m f)
+ with 0 => fun _ _ f => f
+ | S k' => fun _ _ f => m _ _ (POW k' m f)
end.
Module Type BushkToList_Type.
diff --git a/test-suite/bugs/closed/shouldsucceed/1925.v b/test-suite/bugs/closed/shouldsucceed/1925.v
index 17eb721a..4caee1c3 100644
--- a/test-suite/bugs/closed/shouldsucceed/1925.v
+++ b/test-suite/bugs/closed/shouldsucceed/1925.v
@@ -3,14 +3,14 @@
Require Import List.
-Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C :=
+Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C :=
fun x : A => g(f x).
-Definition map_fuse' :
- forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A),
- (map g (map f xs)) = map (compose _ _ _ g f) xs
+Definition map_fuse' :
+ forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A),
+ (map g (map f xs)) = map (compose _ _ _ g f) xs
:=
- fun A B C g f =>
+ fun A B C g f =>
(fix loop (ys : list A) {struct ys} :=
match ys as ys return (map g (map f ys)) = map (compose _ _ _ g f) ys
with
diff --git a/test-suite/bugs/closed/shouldsucceed/1931.v b/test-suite/bugs/closed/shouldsucceed/1931.v
index bc8be78f..930ace1d 100644
--- a/test-suite/bugs/closed/shouldsucceed/1931.v
+++ b/test-suite/bugs/closed/shouldsucceed/1931.v
@@ -8,7 +8,7 @@ Inductive T (A:Set) : Set :=
Fixpoint map (A B:Set)(f:A->B)(t:T A) : T B :=
match t with
app t1 t2 => app (map f t1)(map f t2)
- end.
+ end.
Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B :=
match t with
@@ -19,7 +19,7 @@ Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B :=
Definition k0:=Set.
(** interaction of subst with map *)
-Lemma substLaw1 (A:k0)(B C:Set)(f: A -> B)(g:B -> T C)(t: T A):
+Lemma substLaw1 (A:k0)(B C:Set)(f: A -> B)(g:B -> T C)(t: T A):
subst g (map f t) = subst (fun x => g (f x)) t.
Proof.
intros.
diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v
index 641dcb7a..72396d49 100644
--- a/test-suite/bugs/closed/shouldsucceed/1935.v
+++ b/test-suite/bugs/closed/shouldsucceed/1935.v
@@ -1,14 +1,14 @@
Definition f (n:nat) := n = n.
Lemma f_refl : forall n , f n.
-intros. reflexivity.
+intros. reflexivity.
Qed.
Definition f' (x:nat) (n:nat) := n = n.
Lemma f_refl' : forall n , f' n n.
Proof.
- intros. reflexivity.
+ intros. reflexivity.
Qed.
Require Import ZArith.
diff --git a/test-suite/bugs/closed/shouldsucceed/1939.v b/test-suite/bugs/closed/shouldsucceed/1939.v
new file mode 100644
index 00000000..5e61529b
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1939.v
@@ -0,0 +1,19 @@
+Require Import Setoid Program.Basics.
+
+ Parameter P : nat -> Prop.
+ Parameter R : nat -> nat -> Prop.
+
+ Add Parametric Morphism : P
+ with signature R ++> impl as PM1.
+ Admitted.
+
+ Add Parametric Morphism : P
+ with signature R --> impl as PM2.
+ Admitted.
+
+ Goal forall x y, R x y -> P y -> P x.
+ Proof.
+ intros x y H1 H2.
+ rewrite H1.
+ auto.
+ Qed. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1944.v b/test-suite/bugs/closed/shouldsucceed/1944.v
new file mode 100644
index 00000000..ee2918c6
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1944.v
@@ -0,0 +1,9 @@
+(* Test some uses of ? in introduction patterns *)
+
+Inductive J : nat -> Prop :=
+ | K : forall p, J p -> (True /\ True) -> J (S p).
+
+Lemma bug : forall n, J n -> J (S n).
+Proof.
+ intros ? H.
+ induction H as [? ? [? ?]].
diff --git a/test-suite/bugs/closed/shouldsucceed/1951.v b/test-suite/bugs/closed/shouldsucceed/1951.v
new file mode 100644
index 00000000..12c0ef9b
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1951.v
@@ -0,0 +1,63 @@
+
+(* First a simplification of the bug *)
+
+Set Printing Universes.
+
+Inductive enc (A:Type (*1*)) (* : Type.1 *) := C : A -> enc A.
+
+Definition id (X:Type(*5*)) (x:X) := x.
+
+Lemma test : let S := Type(*6 : 7*) in enc S -> S.
+simpl; intros.
+apply enc.
+apply id.
+apply Prop.
+Defined.
+
+(* Then the original bug *)
+
+Require Import List.
+
+Inductive a : Set := (* some dummy inductive *)
+b : (list a) -> a. (* i don't know if this *)
+ (* happens for smaller *)
+ (* ones *)
+
+Inductive sg : Type := Sg. (* single *)
+
+Definition ipl2 (P : a -> Type) := (* in Prop, that means P is true forall *)
+fold_right (fun x => prod (P x)) sg. (* the elements of a given list *)
+
+Definition ind
+ : forall S : a -> Type,
+ (forall ls : list a, ipl2 S ls -> S (b ls)) -> forall s : a, S s :=
+fun (S : a -> Type)
+ (X : forall ls : list a, ipl2 S ls -> S (b ls)) =>
+fix ind2 (s : a) :=
+match s as a return (S a) with
+| b l =>
+ X l
+ (list_rect (fun l0 : list a => ipl2 S l0) Sg
+ (fun (a0 : a) (l0 : list a) (IHl : ipl2 S l0) =>
+ pair (ind2 a0) IHl) l)
+end. (* some induction principle *)
+
+Implicit Arguments ind [S].
+
+Lemma k : a -> Type. (* some ininteresting lemma *)
+intro;pattern H;apply ind;intros.
+ assert (K : Type).
+ induction ls.
+ exact sg.
+ exact sg.
+ exact (prod K sg).
+Defined.
+
+Lemma k' : a -> Type. (* same lemma but with our bug *)
+intro;pattern H;apply ind;intros.
+ apply prod.
+ induction ls.
+ exact sg.
+ exact sg.
+ exact sg. (* Proof complete *)
+Defined. (* bug *)
diff --git a/test-suite/bugs/closed/shouldsucceed/1981.v b/test-suite/bugs/closed/shouldsucceed/1981.v
index 0c3b96da..99952682 100644
--- a/test-suite/bugs/closed/shouldsucceed/1981.v
+++ b/test-suite/bugs/closed/shouldsucceed/1981.v
@@ -1,5 +1,5 @@
Implicit Arguments ex_intro [A].
Goal exists n : nat, True.
- eapply ex_intro. exact 0. exact I.
+ eapply ex_intro. exact 0. exact I.
Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2001.v b/test-suite/bugs/closed/shouldsucceed/2001.v
index 323021de..d0b3bf17 100644
--- a/test-suite/bugs/closed/shouldsucceed/2001.v
+++ b/test-suite/bugs/closed/shouldsucceed/2001.v
@@ -1,8 +1,10 @@
(* Automatic computing of guard in "Theorem with"; check that guard is not
computed when the user explicitly indicated it *)
+Unset Automatic Introduction.
+
Inductive T : Set :=
-| v : T.
+| v : T.
Definition f (s:nat) (t:T) : nat.
fix 2.
@@ -12,9 +14,9 @@ refine
| v => s
end.
Defined.
-
+
Lemma test :
forall s, f s v = s.
-Proof.
+Proof.
reflexivity.
-Qed.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2017.v b/test-suite/bugs/closed/shouldsucceed/2017.v
index 948cea3e..df666148 100644
--- a/test-suite/bugs/closed/shouldsucceed/2017.v
+++ b/test-suite/bugs/closed/shouldsucceed/2017.v
@@ -8,8 +8,8 @@ Set Implicit Arguments.
Variable choose : forall(P : bool -> Prop)(H : exists x, P x), bool.
Variable H : exists x : bool, True.
-
+
Definition coef :=
match Some true with
- Some _ => @choose _ H |_ => true
-end .
+ Some _ => @choose _ H |_ => true
+end .
diff --git a/test-suite/bugs/closed/shouldsucceed/2083.v b/test-suite/bugs/closed/shouldsucceed/2083.v
new file mode 100644
index 00000000..a6ce4de0
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2083.v
@@ -0,0 +1,27 @@
+Require Import Program Arith.
+
+Program Fixpoint check_n (n : nat) (P : { i | i < n } -> bool) (p : nat)
+ (H : forall (i : { i | i < n }), i < p -> P i = true)
+ {measure (n - p)} :
+ Exc (forall (p : { i | i < n}), P p = true) :=
+ match le_lt_dec n p with
+ | left _ => value _
+ | right cmp =>
+ if dec (P p) then
+ check_n n P (S p) _
+ else
+ error
+ end.
+
+Require Import Omega.
+
+Solve Obligations using program_simpl ; auto with *; try omega.
+
+Next Obligation.
+ apply H. simpl. omega.
+Defined.
+
+Next Obligation.
+ case (le_lt_dec p i) ; intros. assert(i = p) by omega. subst.
+ revert H0. clear_subset_proofs. auto.
+ apply H. simpl. assumption. Defined.
diff --git a/test-suite/bugs/closed/shouldsucceed/2095.v b/test-suite/bugs/closed/shouldsucceed/2095.v
new file mode 100644
index 00000000..28ea99df
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2095.v
@@ -0,0 +1,19 @@
+(* Classes and sections *)
+
+Section OPT.
+ Variable A: Type.
+
+ Inductive MyOption: Type :=
+ | MyNone: MyOption
+ | MySome: A -> MyOption.
+
+ Class Opt: Type := {
+ f_opt: A -> MyOption
+ }.
+End OPT.
+
+Definition f_nat (n: nat): MyOption nat := MySome _ n.
+
+Instance Nat_Opt: Opt nat := {
+ f_opt := f_nat
+}.
diff --git a/test-suite/bugs/closed/shouldsucceed/2108.v b/test-suite/bugs/closed/shouldsucceed/2108.v
new file mode 100644
index 00000000..cad8baa9
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2108.v
@@ -0,0 +1,22 @@
+(* Declare Module in Module Type *)
+Module Type A.
+Record t : Set := { something : unit }.
+End A.
+
+
+Module Type B.
+Declare Module BA : A.
+End B.
+
+
+Module Type C.
+Declare Module CA : A.
+Declare Module CB : B with Module BA := CA.
+End C.
+
+
+Module Type D.
+Declare Module DA : A.
+(* Next line gives: "Anomaly: uncaught exception Not_found. Please report." *)
+Declare Module DC : C with Module CA := DA.
+End D.
diff --git a/test-suite/bugs/closed/shouldsucceed/2117.v b/test-suite/bugs/closed/shouldsucceed/2117.v
new file mode 100644
index 00000000..6377a8b7
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2117.v
@@ -0,0 +1,56 @@
+(* Check pattern-unification on evars in apply unification *)
+
+Axiom app : forall tau tau':Type, (tau -> tau') -> tau -> tau'.
+
+Axiom copy : forall tau:Type, tau -> tau -> Prop.
+Axiom copyr : forall tau:Type, tau -> tau -> Prop.
+Axiom copyf : forall tau:Type, tau -> tau -> Prop.
+Axiom eq : forall tau:Type, tau -> tau -> Prop.
+Axiom subst : forall tau tau':Type, (tau -> tau') -> tau -> tau' -> Prop.
+
+Axiom copy_atom : forall tau:Type, forall t t':tau, eq tau t t' -> copy tau t t'.
+Axiom copy_fun: forall tau tau':Type, forall t t':(tau->tau'),
+(forall x:tau, copyr tau x x->copy tau' (t x) (t' x))
+->copy (tau->tau') t t'.
+
+Axiom copyr_atom : forall tau:Type, forall t t':tau, copyr tau t t' -> eq tau t t'.
+Axiom copyr_fun: forall tau tau':Type, forall t t':(tau->tau'),
+copyr (tau->tau') t t'
+->(forall x y:tau, copy tau x y->copyr tau' (t x) (t' y)).
+
+Axiom copyf_atom : forall tau:Type, forall t t':tau, copyf tau t t' -> eq tau t t'.
+Axiom copyf_fun: forall tau tau':Type, forall t t':(tau->tau'),
+copyr (tau->tau') t t'
+->(forall x y:tau, forall z1 z2:tau',
+(copy tau x y)->
+(subst tau tau' t x z1)->
+(subst tau tau' t' y z2)->
+copyf tau' z1 z2).
+
+Axiom eqappg: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',forall t':tau',
+( ((subst tau tau' t q t') /\ (eq tau' t' r))
+->eq tau' (app tau tau' t q) r).
+
+Axiom eqappd: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',
+forall t':tau', ((subst tau tau' t q t') /\ (eq tau' r t'))
+->eq tau' r (app tau tau' t q).
+
+Axiom substcopy: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',
+(forall x:tau, (copyf tau x q) -> (copy tau' (t x) r))
+->subst tau tau' t q r.
+
+Ltac EtaLong := (apply copy_fun;intros;EtaLong)|| apply copy_atom.
+Ltac Subst := apply substcopy;intros;EtaLong.
+Ltac Rigid_aux := fun A => apply A|| Rigid_aux (copyr_fun _ _ _ _ A).
+Ltac Rigid := fun A => apply copyr_atom; Rigid_aux A.
+
+Theorem church0: forall i:Type, exists X:(i->i)->i->i,
+copy ((i->i)->i->i) (fun f:i->i => fun x:i=>f (X f x)) (fun f:i->i=>fun x:i=>app i i (X f) (f x)).
+intros.
+esplit.
+EtaLong.
+eapply eqappd;split.
+Subst.
+apply copyf_atom.
+Show Existentials.
+apply H1.
diff --git a/test-suite/bugs/closed/shouldsucceed/2123.v b/test-suite/bugs/closed/shouldsucceed/2123.v
new file mode 100644
index 00000000..422a2c12
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2123.v
@@ -0,0 +1,11 @@
+(* About the detection of non-dependent metas by the refine tactic *)
+
+(* The following is a simplification of bug #2123 *)
+
+Parameter fset : nat -> Set.
+Parameter widen : forall (n : nat) (s : fset n), { x : fset (S n) | s=s }.
+Goal forall i, fset (S i).
+intro.
+refine (proj1_sig (widen i _)).
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2127.v b/test-suite/bugs/closed/shouldsucceed/2127.v
new file mode 100644
index 00000000..20ea4603
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2127.v
@@ -0,0 +1,11 @@
+(* Check that "apply refl_equal" 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.
+End A.
+
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2135.v b/test-suite/bugs/closed/shouldsucceed/2135.v
new file mode 100644
index 00000000..61882176
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2135.v
@@ -0,0 +1,9 @@
+(* Check that metas are whd-normalized before trying 2nd-order unification *)
+Lemma test :
+ forall (D:Type) (T : forall C, option C) (Q:forall D, option D -> Prop),
+ (forall (A : Type) (P : forall B:Type, option B -> Prop), P A (T A))
+ -> Q D (T D).
+Proof.
+ intros D T Q H.
+ pattern (T D). apply H.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2136.v b/test-suite/bugs/closed/shouldsucceed/2136.v
new file mode 100644
index 00000000..d2b926f3
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2136.v
@@ -0,0 +1,61 @@
+(* Bug #2136
+
+The fsetdec tactic seems to get confused by hypotheses like
+ HeqH1 : H1 = MkEquality s0 s1 b
+If I clear them then it is able to solve my goal; otherwise it is not.
+I would expect it to be able to solve the goal even without this hypothesis
+being cleared. A small, self-contained example is below.
+
+I have coq r12238.
+
+
+Thanks
+Ian
+*)
+
+
+Require Import FSets.
+Require Import Arith.
+Require Import FSetWeakList.
+
+Module DecidableNat.
+Definition t := nat.
+Definition eq := @eq nat.
+Definition eq_refl := @refl_equal nat.
+Definition eq_sym := @sym_eq nat.
+Definition eq_trans := @trans_eq nat.
+Definition eq_dec := eq_nat_dec.
+End DecidableNat.
+
+Module NatSet := Make(DecidableNat).
+
+Module Export Dec := WDecide (NatSet).
+Import FSetDecideAuxiliary.
+
+Parameter MkEquality : forall ( s0 s1 : NatSet.t )
+ ( x : nat ),
+ NatSet.Equal s1 (NatSet.add x s0).
+
+Lemma ThisLemmaWorks : forall ( s0 s1 : NatSet.t )
+ ( a b : nat ),
+ NatSet.In a s0
+ -> NatSet.In a s1.
+Proof.
+intros.
+remember (MkEquality s0 s1 b) as H1.
+clear HeqH1.
+fsetdec.
+Qed.
+
+Lemma ThisLemmaWasFailing : forall ( s0 s1 : NatSet.t )
+ ( a b : nat ),
+ NatSet.In a s0
+ -> NatSet.In a s1.
+Proof.
+intros.
+remember (MkEquality s0 s1 b) as H1.
+fsetdec.
+(*
+Error: Tactic failure: because the goal is beyond the scope of this tactic.
+*)
+Qed. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2137.v b/test-suite/bugs/closed/shouldsucceed/2137.v
new file mode 100644
index 00000000..6c2023ab
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2137.v
@@ -0,0 +1,52 @@
+(* Bug #2137
+
+The fsetdec tactic is sensitive to which way round the arguments to <> are.
+In the small, self-contained example below, it is able to solve the goal
+if it knows that "b <> a", but not if it knows that "a <> b". I would expect
+it to be able to solve hte goal in either case.
+
+I have coq r12238.
+
+
+Thanks
+Ian
+
+*)
+
+Require Import Arith FSets FSetWeakList.
+
+Module DecidableNat.
+Definition t := nat.
+Definition eq := @eq nat.
+Definition eq_refl := @refl_equal nat.
+Definition eq_sym := @sym_eq nat.
+Definition eq_trans := @trans_eq nat.
+Definition eq_dec := eq_nat_dec.
+End DecidableNat.
+
+Module NatSet := Make(DecidableNat).
+
+Module Export NameSetDec := WDecide (NatSet).
+
+Lemma ThisLemmaWorks : forall ( s0 : NatSet.t )
+ ( a b : nat ),
+ b <> a
+ -> ~(NatSet.In a s0)
+ -> ~(NatSet.In a (NatSet.add b s0)).
+Proof.
+intros.
+fsetdec.
+Qed.
+
+Lemma ThisLemmaWasFailing : forall ( s0 : NatSet.t )
+ ( a b : nat ),
+ a <> b
+ -> ~(NatSet.In a s0)
+ -> ~(NatSet.In a (NatSet.add b s0)).
+Proof.
+intros.
+fsetdec.
+(*
+Error: Tactic failure: because the goal is beyond the scope of this tactic.
+*)
+Qed. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2139.v b/test-suite/bugs/closed/shouldsucceed/2139.v
new file mode 100644
index 00000000..a7f35508
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2139.v
@@ -0,0 +1,24 @@
+(* Call of apply on <-> failed because of evars in elimination predicate *)
+Generalizable Variables patch.
+
+Class Patch (patch : Type) := {
+ commute : patch -> patch -> Prop
+}.
+
+Parameter flip : forall `{patchInstance : Patch patch}
+ {a b : patch},
+ commute a b <-> commute b a.
+
+Lemma Foo : forall `{patchInstance : Patch patch}
+ {a b : patch},
+ (commute a b)
+ -> True.
+Proof.
+intros.
+apply flip in H.
+
+(* failed in well-formed arity check because elimination predicate of
+ iff in (@flip _ _ _ _) had normalized evars while the ones in the
+ type of (@flip _ _ _ _) itself had non-normalized evars *)
+
+(* By the way, is the check necessary ? *)
diff --git a/test-suite/bugs/closed/shouldsucceed/2145.v b/test-suite/bugs/closed/shouldsucceed/2145.v
new file mode 100644
index 00000000..b6c5da65
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2145.v
@@ -0,0 +1,20 @@
+(* Test robustness of Groebner tactic in presence of disequalities *)
+
+Require Export Reals.
+Require Export NsatzR.
+
+Open Scope R_scope.
+
+Lemma essai :
+ forall yb xb m1 m2 xa ya,
+ xa <> xb ->
+ yb - 2 * m2 * xb = ya - m2 * xa ->
+ yb - m1 * xb = ya - m1 * xa ->
+ yb - ya = (2 * xb - xa) * m2 ->
+ yb - ya = (xb - xa) * m1.
+Proof.
+intros.
+(* clear H. groebner used not to work when H was not cleared *)
+nsatzR.
+Qed.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/2193.v b/test-suite/bugs/closed/shouldsucceed/2193.v
new file mode 100644
index 00000000..fe258867
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2193.v
@@ -0,0 +1,31 @@
+(* Computation of dependencies in the "match" return predicate was incomplete *)
+(* Submitted by R. O'Connor, Nov 2009 *)
+
+Inductive Symbol : Set :=
+ | VAR : Symbol.
+
+Inductive SExpression :=
+ | atomic : Symbol -> SExpression.
+
+Inductive ProperExpr : SExpression -> SExpression -> Type :=
+ | pe_3 : forall (x : Symbol) (alpha : SExpression),
+ ProperExpr alpha (atomic VAR) ->
+ ProperExpr (atomic x) alpha.
+
+Definition A (P : forall s : SExpression, Type)
+ (x alpha alpha1 : SExpression)
+ (t : ProperExpr (x) alpha1) : option (x = atomic VAR) :=
+ match t as pe in ProperExpr a b return option (a = atomic VAR) with
+ | pe_3 x0 alpha3 tye' =>
+ (fun (x:Symbol) (alpha : SExpression) => @None (atomic x = atomic VAR))
+ x0 alpha3
+ end.
+
+Definition B (P : forall s : SExpression, Type)
+ (x alpha alpha1 : SExpression)
+ (t : ProperExpr (x) alpha1) : option (x = atomic VAR) :=
+ match t as pe in ProperExpr a b return option (a = atomic VAR) with
+ | pe_3 x0 alpha3 tye' =>
+ (fun (x:Symbol) (alpha : SExpression) (t:ProperExpr alpha (atomic VAR)) => @None (atomic x = atomic VAR))
+ x0 alpha3 tye'
+ end.
diff --git a/test-suite/bugs/closed/shouldsucceed/2231.v b/test-suite/bugs/closed/shouldsucceed/2231.v
new file mode 100644
index 00000000..03e2c9bb
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2231.v
@@ -0,0 +1,3 @@
+Inductive unit2 : Type := U : unit -> unit2.
+Inductive dummy (u: unit2) : unit -> Type :=
+ V: dummy u (let (tt) := u in tt).
diff --git a/test-suite/bugs/closed/shouldsucceed/2244.v b/test-suite/bugs/closed/shouldsucceed/2244.v
new file mode 100644
index 00000000..d499e515
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2244.v
@@ -0,0 +1,19 @@
+(* 1st-order unification did not work when in competition with pattern unif. *)
+
+Set Implicit Arguments.
+Lemma test : forall
+ (A : Type)
+ (B : Type)
+ (f : A -> B)
+ (S : B -> Prop)
+ (EV : forall y (f':A->B), (forall x', S (f' x')) -> S (f y))
+ (HS : forall x', S (f x'))
+ (x : A),
+ S (f x).
+Proof.
+ intros. eapply EV. intros.
+ (* worked in v8.2 but not in v8.3beta, fixed in r12898 *)
+ apply HS.
+
+ (* still not compatible with 8.2 because an evar can be solved in
+ two different ways and is left open *)
diff --git a/test-suite/bugs/closed/shouldsucceed/2255.v b/test-suite/bugs/closed/shouldsucceed/2255.v
new file mode 100644
index 00000000..bf80ff66
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2255.v
@@ -0,0 +1,21 @@
+(* Check injection in presence of dependencies hidden in applicative terms *)
+
+Inductive TupleT : nat -> Type :=
+ nilT : TupleT 0
+| consT {n} A : (A -> TupleT n) -> TupleT (S n).
+
+Inductive Tuple : forall n, TupleT n -> Type :=
+ nil : Tuple _ nilT
+| cons {n} A (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F).
+
+Goal forall n A F x X n0 A0 x0 F0 H0 (H : existT (fun n0 : nat => {H0 : TupleT
+n0 & Tuple n0 H0})
+ (S n0)
+ (existT (fun H0 : TupleT (S n0) => Tuple (S n0) H0)
+ (consT A0 F0) (cons A0 x0 F0 H0)) =
+ existT (fun n0 : nat => {H0 : TupleT n0 & Tuple n0 H0})
+ (S n)
+ (existT (fun H0 : TupleT (S n) => Tuple (S n) H0)
+ (consT A F) (cons A x F X))), False.
+intros.
+injection H.
diff --git a/test-suite/bugs/closed/shouldsucceed/2281.v b/test-suite/bugs/closed/shouldsucceed/2281.v
new file mode 100644
index 00000000..40948d90
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2281.v
@@ -0,0 +1,50 @@
+(** Bug #2281
+
+In the code below, coq is confused by an equality unless it is first 'subst'ed
+away, yet http://coq.inria.fr/stdlib/Coq.FSets.FSetDecide.html says
+
+ fsetdec will first perform any necessary zeta and beta reductions and will
+invoke subst to eliminate any Coq equalities between finite sets or their
+elements.
+
+I have coq r12851.
+
+*)
+
+Require Import Arith.
+Require Import FSets.
+Require Import FSetWeakList.
+
+Module DecidableNat.
+Definition t := nat.
+Definition eq := @eq nat.
+Definition eq_refl := @refl_equal nat.
+Definition eq_sym := @sym_eq nat.
+Definition eq_trans := @trans_eq nat.
+Definition eq_dec := eq_nat_dec.
+End DecidableNat.
+
+Module NatSet := Make(DecidableNat).
+
+Module Export NameSetDec := WDecide (NatSet).
+
+Lemma ThisLemmaWorks : forall ( s1 s2 : NatSet.t )
+ ( H : s1 = s2 ),
+ NatSet.Equal s1 s2.
+Proof.
+intros.
+subst.
+fsetdec.
+Qed.
+
+Import FSetDecideAuxiliary.
+
+Lemma ThisLemmaWasFailing : forall ( s1 s2 : NatSet.t )
+ ( H : s1 = s2 ),
+ NatSet.Equal s1 s2.
+Proof.
+intros.
+fsetdec.
+(* Error: Tactic failure: because the goal is beyond the scope of this tactic.
+*)
+Qed. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2295.v b/test-suite/bugs/closed/shouldsucceed/2295.v
new file mode 100644
index 00000000..f5ca28dc
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2295.v
@@ -0,0 +1,11 @@
+(* Check if omission of "as" in return clause works w/ section variables too *)
+
+Section sec.
+
+Variable b: bool.
+
+Definition d' :=
+ (match b return b = true \/ b = false with
+ | true => or_introl _ (refl_equal true)
+ | false => or_intror _ (refl_equal false)
+ end).
diff --git a/test-suite/bugs/closed/shouldsucceed/2299.v b/test-suite/bugs/closed/shouldsucceed/2299.v
new file mode 100644
index 00000000..c0552ca7
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2299.v
@@ -0,0 +1,13 @@
+(* Check that destruct refreshes universes in what it generalizes *)
+
+Section test.
+
+Variable A: Type.
+
+Inductive T: unit -> Type := C: A -> unit -> T tt.
+
+Let unused := T tt.
+
+Goal T tt -> False.
+ intro X.
+ destruct X.
diff --git a/test-suite/bugs/closed/shouldsucceed/2300.v b/test-suite/bugs/closed/shouldsucceed/2300.v
new file mode 100644
index 00000000..4e587cbb
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2300.v
@@ -0,0 +1,15 @@
+(* Check some behavior of Ltac pattern-matching wrt universe levels *)
+
+Section contents.
+
+Variables (A: Type) (B: (unit -> Type) -> Type).
+
+Inductive C := c: A -> unit -> C.
+
+Let unused2 (x: unit) := C.
+
+Goal True.
+intuition.
+Qed.
+
+End contents.
diff --git a/test-suite/bugs/closed/shouldsucceed/335.v b/test-suite/bugs/closed/shouldsucceed/335.v
new file mode 100644
index 00000000..166fa7a9
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/335.v
@@ -0,0 +1,5 @@
+(* Compatibility of Require with backtracking at interactive module end *)
+
+Module A.
+Require List.
+End A.
diff --git a/test-suite/bugs/closed/shouldsucceed/38.v b/test-suite/bugs/closed/shouldsucceed/38.v
index 7bc04b1f..4fc8d7c9 100644
--- a/test-suite/bugs/closed/shouldsucceed/38.v
+++ b/test-suite/bugs/closed/shouldsucceed/38.v
@@ -6,7 +6,7 @@ Inductive liste : Set :=
| vide : liste
| c : A -> liste -> liste.
-Inductive e : A -> liste -> Prop :=
+Inductive e : A -> liste -> Prop :=
| ec : forall (x : A) (l : liste), e x (c x l)
| ee : forall (x y : A) (l : liste), e x l -> e x (c y l).
diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v
index a963b225..ee5ec1fa 100644
--- a/test-suite/bugs/closed/shouldsucceed/846.v
+++ b/test-suite/bugs/closed/shouldsucceed/846.v
@@ -27,7 +27,7 @@ Definition index := list bool.
Inductive L (A:Set) : index -> Set :=
initL: A -> L A nil
- | pluslL: forall l:index, One -> L A (false::l)
+ | pluslL: forall l:index, One -> L A (false::l)
| plusrL: forall l:index, L A l -> L A (false::l)
| varL: forall l:index, L A l -> L A (true::l)
| appL: forall l:index, L A (true::l) -> L A (true::l) -> L A (true::l)
@@ -109,7 +109,7 @@ Proof.
exact (monL (fun x:One + A =>
(match (maybe (fun a:A => initL a) x) with
| inl u => pluslL _ _ u
- | inr t' => plusrL t' end)) r).
+ | inr t' => plusrL t' end)) r).
Defined.
Section minimal.
@@ -119,11 +119,11 @@ Hypothesis G: Set -> Set.
Hypothesis step: sub1 (LamF' G) G.
Fixpoint L'(A:Set)(i:index){struct i} : Set :=
- match i with
+ match i with
nil => A
| false::l => One + L' A l
| true::l => G (L' A l)
- end.
+ end.
Definition LinL': forall (A:Set)(i:index), L A i -> L' A i.
Proof.
@@ -177,7 +177,7 @@ Proof.
assumption.
induction a.
simpl L' in t.
- apply (aczelapp (l1:=true::nil) (l2:=i)).
+ apply (aczelapp (l1:=true::nil) (l2:=i)).
exact (lam' IHi t).
simpl L' in t.
induction t.