Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

21 files changed, 629 insertions, 89 deletions

diff --git a/test-suite/failure/Uminus.v b/test-suite/failure/Uminus.v
new file mode 100644
index 00000000..6866f19a
--- /dev/null
+++ b/test-suite/failure/Uminus.v
@@ -0,0 +1,62 @@
+(* Check that the encoding of system U- fails *)
+
+Inductive prop : Prop := down : Prop -> prop.
+
+Definition up (p:prop) : Prop := let (A) := p in A.
+
+Lemma p2p1 : forall A:Prop, up (down A) -> A.
+Proof.
+exact (fun A x => x).
+Qed.
+
+Lemma p2p2 : forall A:Prop, A -> up (down A).
+Proof.
+exact (fun A x => x).
+Qed.
+
+(** Hurkens' paradox *)
+
+Definition V := forall A:Prop, ((A -> prop) -> A -> prop) -> A -> prop.
+Definition U := V -> prop.
+Definition sb (z:V) : V := fun A r a => r (z A r) a.
+Definition le (i:U -> prop) (x:U) : prop :=
+  x (fun A r a => i (fun v => sb v A r a)).
+Definition induct (i:U -> prop) : Prop :=
+  forall x:U, up (le i x) -> up (i x).
+Definition WF : U := fun z => down (induct (z U le)).
+Definition I (x:U) : Prop :=
+  (forall i:U -> prop, up (le i x) -> up (i (fun v => sb v U le x))) -> False.
+
+Lemma Omega : forall i:U -> prop, induct i -> up (i WF).
+Proof.
+intros i y.
+apply y.
+unfold le, WF, induct in |- *.
+intros x H0.
+apply y.
+exact H0.
+Qed.
+
+Lemma lemma1 : induct (fun u => down (I u)).
+Proof.
+unfold induct in |- *.
+intros x p.
+intro q.
+apply (q (fun u => down (I u)) p).
+intro i.
+apply q with (i := fun y => i (fun v:V => sb v U le y)).
+Qed.
+
+Lemma lemma2 : (forall i:U -> prop, induct i -> up (i WF)) -> False.
+Proof.
+intro x.
+apply (x (fun u => down (I u)) lemma1).
+intros i H0.
+apply (x (fun y => i (fun v => sb v U le y))).
+apply H0.
+Qed.
+
+Theorem paradox : False.
+Proof.
+exact (lemma2 Omega).
+Qed.
diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v
index aad493ce..b886eb59 100644
--- a/test-suite/modules/mod_decl.v
+++ b/test-suite/modules/mod_decl.v
@@ -34,7 +34,7 @@ Module Type T.
   
   Declare Module M1: SIG.
   
-  Declare Module M2 <: SIG.
+  Module M2 <: SIG.
     Definition A := nat.
   End M2.
   
diff --git a/test-suite/modules/objects2.v b/test-suite/modules/objects2.v
new file mode 100644
index 00000000..e286609e
--- /dev/null
+++ b/test-suite/modules/objects2.v
@@ -0,0 +1,11 @@
+(* Check that non logical object loading is done after registration of
+   the logical objects in the environment
+*)
+
+(* Bug #1118 (simplified version), submitted by Evelyne Contejean
+  (used to failed in pre-V8.1 trunk because of a call to lookup_mind
+   for structure objects) 
+*)
+
+Module Type S. Record t : Set := { a : nat; b : nat }. End S.
+Module Make (X:S). Module Y:=X. End Make.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 63137edb..a3033e94 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -2,7 +2,7 @@ t_rect =
 fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
 fix F (t : t) : P t :=
   match t as t0 return (P t0) with
-  | k x x0 => f x0 (F x0)
+  | k _ x0 => f x0 (F x0)
   end
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index 4ed72c50..c7f3ed7d 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,4 +1,4 @@
-Inductive sig2 (A : Set) (P : A -> Prop) (Q : A -> Prop) : Set :=
+Inductive sig2 (A : Type) (P : A -> Prop) (Q : A -> Prop) : Type :=
     exist2 : forall x : A, P x -> Q x -> sig2 P Q
 For sig2: Argument A is implicit
 For exist2: Argument A is implicit
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 71c59e43..8e8b8059 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -1 +1,4 @@
 intro H; split; [  a H |  e H ].
+intros; match goal with
+        | |- context [if ?X then _ else _] => case X
+        end; trivial.
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index 24a33651..8fa91994 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -7,3 +7,12 @@ Lemma test : True -> True /\ True.
 intro H; split; [a H|e H].
 Show Script.
 Qed.
+
+(* Test printing of match context *)
+(* Used to fail after translator removal (see bug #1070) *)
+
+Lemma test2 : forall n:nat, forall f: nat -> bool, O = if (f n) then O else O.
+Proof.
+intros;match goal with |- context [if ?X then _ else _ ] => case X end;trivial.
+Show Script.
+Qed.
diff --git a/test-suite/success/Destruct.v b/test-suite/success/Destruct.v
deleted file mode 100644
index b909e45e..00000000
--- a/test-suite/success/Destruct.v
+++ /dev/null
@@ -1,13 +0,0 @@
-(* Submitted by Robert Schneck *)
-
-Parameter A B C D : Prop.
-Axiom X : A -> B -> C /\ D.
-
-Lemma foo : A -> B -> C.
-Proof.
-intros. 
-destruct X. (* Should find axiom X and should handle arguments of X *)
-assumption.
-assumption.
-assumption.
-Qed.
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index 84a58a3a..939d06c7 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -5,25 +5,17 @@ Definition iszero (n : nat) : bool :=
   | _ => false
   end.
 
- Functional Scheme iszer_ind := Induction for iszero.
+Functional Scheme iszero_ind := Induction for iszero Sort Prop.
  
 Lemma toto : forall n : nat, n = 0 -> iszero n = true.
 intros x eg.
  functional induction iszero x; simpl in |- *.
 trivial.
- subst x.
-inversion H_eq_.
+inversion eg.
 Qed.
 
-(* We can even reuse the proof as a scheme: *)
-
- Functional Scheme toto_ind := Induction for iszero.
-
-
-
-
  
-Definition ftest (n m : nat) : nat :=
+Function ftest (n m : nat) : nat :=
   match n with
   | O => match m with
          | O => 0
@@ -32,27 +24,25 @@ Definition ftest (n m : nat) : nat :=
   | S p => 0
   end.
 
- Functional Scheme ftest_ind := Induction for ftest. 
-
 Lemma test1 : forall n m : nat, ftest n m <= 2.
 intros n m.
  functional induction ftest n m; auto.
 Qed.
 
-
+Require Import Arith.
 Lemma test11 : forall m : nat, ftest 0 m <= 2.
 intros m.
  functional induction ftest 0 m.
 auto. 
-auto. 
+auto.
+auto with *. 
 Qed.
 
-
-Definition lamfix (m : nat) :=
-  fix trivfun (n : nat) : nat := match n with
-                                 | O => m
-                                 | S p => trivfun p
-                                 end.
+Function lamfix (m n : nat) {struct n } : nat :=
+  match n with
+    | O => m
+    | S p => lamfix m p
+  end.
 
 (* Parameter v1 v2 : nat. *)
 
@@ -68,12 +58,12 @@ Defined.
 (* polymorphic function *)
 Require Import List.
 
- Functional Scheme app_ind := Induction for app.
+Functional Scheme app_ind := Induction for app Sort Prop.
 
 Lemma appnil : forall (A : Set) (l l' : list A), l' = nil -> l = l ++ l'.
 intros A l l'.
  functional induction app A l l';  intuition.
- rewrite <- H1; trivial.
+ rewrite <- H0; trivial.
 Qed.
 
 
@@ -83,7 +73,7 @@ Qed.
 Require Export Arith.
 
 
-Fixpoint trivfun (n : nat) : nat :=
+Function trivfun (n : nat) : nat :=
   match n with
   | O => 0
   | S m => trivfun m
@@ -97,18 +87,16 @@ Parameter varessai : nat.
 Lemma first_try : trivfun varessai = 0.
  functional induction trivfun varessai.
 trivial.
-simpl in |- *.
 assumption.
 Defined.
  
 
- Functional Scheme triv_ind := Induction for trivfun.
+ Functional Scheme triv_ind := Induction for trivfun Sort Prop.
 
 Lemma bisrepetita : forall n' : nat, trivfun n' = 0.
 intros n'.
  functional induction trivfun n'.
 trivial.
-simpl in |- *.
 assumption.
 Qed.
 
@@ -118,14 +106,14 @@ Qed.
 
 
 
-Fixpoint iseven (n : nat) : bool :=
+Function iseven (n : nat) : bool :=
   match n with
   | O => true
   | S (S m) => iseven m
   | _ => false
   end.
  
-Fixpoint funex (n : nat) : nat :=
+Function funex (n : nat) : nat :=
   match iseven n with
   | true => n
   | false => match n with
@@ -134,7 +122,7 @@ Fixpoint funex (n : nat) : nat :=
              end
   end.
  
-Fixpoint nat_equal_bool (n m : nat) {struct n} : bool :=
+Function nat_equal_bool (n m : nat) {struct n} : bool :=
   match n with
   | O => match m with
          | O => true
@@ -149,6 +137,7 @@ Fixpoint nat_equal_bool (n m : nat) {struct n} : bool :=
 
 Require Export Div2.
  
+Functional Scheme div2_ind := Induction for div2 Sort Prop.
 Lemma div2_inf : forall n : nat, div2 n <= n.
 intros n.
  functional induction div2 n.
@@ -157,34 +146,27 @@ auto.
 
 apply le_S.
 apply le_n_S.
-exact H.
+exact IHn0.
 Qed.
 
 (* reuse this lemma as a scheme:*)
 
- Functional Scheme div2_ind := Induction for div2_inf.
 
-Fixpoint nested_lam (n : nat) : nat -> nat :=
+Function nested_lam (n : nat) : nat -> nat :=
   match n with
   | O => fun m : nat => 0
   | S n' => fun m : nat => m + nested_lam n' m
   end.
 
- Functional Scheme nested_lam_ind := Induction for nested_lam.
 
 Lemma nest : forall n m : nat, nested_lam n m = n * m.
 intros n m.
- functional induction nested_lam n m; auto.
-Qed.
-
-Lemma nest2 : forall n m : nat, nested_lam n m = n * m.
-intros n m. pattern n, m in |- *. 
-apply nested_lam_ind; simpl in |- *; intros; auto.
+ functional induction nested_lam n m; simpl;auto.
 Qed.
 
  
-Fixpoint essai (x : nat) (p : nat * nat) {struct x} : nat :=
-  let (n, m) := p in
+Function essai (x : nat) (p : nat * nat) {struct x} : nat :=
+  let (n, m) := (p: nat*nat) in
   match n with
   | O => 0
   | S q => match x with
@@ -198,12 +180,12 @@ Lemma essai_essai :
 intros x p.
  functional induction essai x p; intros.
 inversion H.
-simpl in |- *; try abstract auto with arith.
-simpl in |- *; try abstract auto with arith.
+auto with arith.
+ auto with arith.
 Qed.
 
  
-Fixpoint plus_x_not_five'' (n m : nat) {struct n} : nat :=
+Function plus_x_not_five'' (n m : nat) {struct n} : nat :=
   let x := nat_equal_bool m 5 in
   let y := 0 in
   match n with
@@ -218,21 +200,18 @@ Fixpoint plus_x_not_five'' (n m : nat) {struct n} : nat :=
  
 Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x.
 intros a b.
-unfold plus_x_not_five'' in |- *.
  functional induction plus_x_not_five'' a b; intros hyp; simpl in |- *; auto.
 Qed.
  
 Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true.
 intros n m.
-unfold nat_equal_bool in |- *.
  functional induction nat_equal_bool n m; simpl in |- *; intros hyp; auto.
-inversion hyp.
+rewrite <- hyp in H1; simpl in H1;tauto. 
 inversion hyp.
 Qed.
  
 Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m.
 intros n m.
-unfold nat_equal_bool in |- *.
  functional induction nat_equal_bool n m; simpl in |- *; intros eg; auto.
 inversion eg.
 inversion eg.
@@ -242,6 +221,8 @@ Qed.
 Inductive istrue : bool -> Prop :=
     istrue0 : istrue true.
  
+Functional Scheme plus_ind := Induction for plus Sort Prop.
+
 Lemma inf_x_plusxy' : forall x y : nat, x <= x + y.
 intros n m.
  functional induction plus n m; intros.
@@ -264,7 +245,7 @@ intros n.
  functional induction plus 0 n; intros; auto with arith.
 Qed.
 
-Fixpoint mod2 (n : nat) : nat :=
+Function mod2 (n : nat) : nat :=
   match n with
   | O => 0
   | S (S m) => S (mod2 m)
@@ -276,13 +257,13 @@ intros n.
  functional induction mod2 n; simpl in |- *; auto with arith.
 Qed.
  
-Definition isfour (n : nat) : bool :=
+Function isfour (n : nat) : bool :=
   match n with
   | S (S (S (S O))) => true
   | _ => false
   end.
  
-Definition isononeorfour (n : nat) : bool :=
+Function isononeorfour (n : nat) : bool :=
   match n with
   | S O => true
   | S (S (S (S O))) => true
@@ -294,15 +275,22 @@ intros n.
  functional induction isononeorfour n; intros istr; simpl in |- *;
  inversion istr.
 apply istrue0.
+destruct n. inversion istr.
+destruct n. tauto.
+destruct n. inversion istr.
+destruct n. inversion istr.
+destruct n. tauto.
+simpl in *. inversion H1.
 Qed.
  
 Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n).
 intros n.
  functional induction isononeorfour n; intros m istr; inversion istr.
 apply istrue0.
+rewrite H in H0; simpl in H0;tauto.
 Qed.
  
-Definition ftest4 (n m : nat) : nat :=
+Function ftest4 (n m : nat) : nat :=
   match n with
   | O => match m with
          | O => 0
@@ -321,13 +309,20 @@ Qed.
  
 Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2.
 intros n m.
- functional induction ftest4 (S n) m.
+assert ({n0 | n0 = S n}).
+exists (S n);reflexivity.
+destruct H as [n0 H1].
+rewrite <- H1;revert H1.
+ functional induction ftest4 n0 m.
+inversion 1.
+inversion 1.
+
 auto with arith.
 auto with arith.
 Qed.
  
-Definition ftest44 (x : nat * nat) (n m : nat) : nat :=
-  let (p, q) := x in
+Function ftest44 (x : nat * nat) (n m : nat) : nat :=
+  let (p, q) := (x: nat*nat) in
   match n with
   | O => match m with
          | O => 0
@@ -349,7 +344,7 @@ auto with arith.
 auto with arith.
 Qed.
  
-Fixpoint ftest2 (n m : nat) {struct n} : nat :=
+Function ftest2 (n m : nat) {struct n} : nat :=
   match n with
   | O => match m with
          | O => 0
@@ -363,7 +358,7 @@ intros n m.
  functional induction ftest2 n m; simpl in |- *; intros; auto.
 Qed.
  
-Fixpoint ftest3 (n m : nat) {struct n} : nat :=
+Function ftest3 (n m : nat) {struct n} : nat :=
   match n with
   | O => 0
   | S p => match m with
@@ -384,7 +379,7 @@ simpl in |- *.
 auto.
 Qed.
  
-Fixpoint ftest5 (n m : nat) {struct n} : nat :=
+Function ftest5 (n m : nat) {struct n} : nat :=
   match n with
   | O => 0
   | S p => match m with
@@ -405,7 +400,7 @@ simpl in |- *.
 auto.
 Qed.
  
-Definition ftest7 (n : nat) : nat :=
+Function ftest7 (n : nat) : nat :=
   match ftest5 n 0 with
   | O => 0
   | S r => 0
@@ -416,11 +411,10 @@ Lemma essai7 :
    (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2) 
    (n : nat), ftest7 n <= 2.
 intros hyp1 hyp2 n.
-unfold ftest7 in |- *.
  functional induction ftest7 n; auto.
 Qed.
  
-Fixpoint ftest6 (n m : nat) {struct n} : nat :=
+Function ftest6 (n m : nat) {struct n} : nat :=
   match n with
   | O => 0
   | S p => match ftest5 p 0 with
@@ -445,7 +439,6 @@ Qed.
  
 Lemma essai6 : forall n m : nat, ftest6 n m <= 2.
 intros n m.
-unfold ftest6 in |- *.
  functional induction ftest6 n m; simpl in |- *; auto.
 Qed.
 
diff --git a/test-suite/success/If.v b/test-suite/success/If.v
deleted file mode 100644
index b7f06dcf..00000000
--- a/test-suite/success/If.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(* Check correct use of if-then-else predicate annotation (cf bug 690) *)
-
-Check fun b : bool =>
- if b as b0 return (if b0 then b0 = true else b0 = false)
- then refl_equal true
- else refl_equal false.
-
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
new file mode 100644
index 00000000..a9e2c59a
--- /dev/null
+++ b/test-suite/success/Notations.v
@@ -0,0 +1,9 @@
+(* Check that "where" clause behaves as if given independently of the  *)
+(* definition (variant of bug #113? submitted by Assia Mahboubi) *)
+
+Fixpoint plus1 (n m:nat) {struct n} : nat :=
+   match n with
+   | O => m
+   | S p => S (p+m)
+   end
+ where "n + m" := (plus1 n m) : nat_scope.
diff --git a/test-suite/success/Omega0.v b/test-suite/success/Omega0.v
new file mode 100644
index 00000000..4614c90d
--- /dev/null
+++ b/test-suite/success/Omega0.v
@@ -0,0 +1,149 @@
+Require Import ZArith Omega.
+Open Scope Z_scope.
+
+(* Pierre L: examples gathered while debugging romega. *)
+
+Lemma test_romega_0 : 
+ forall m m', 
+  0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
+Proof.
+intros.
+(*omega.*)
+Admitted.
+
+Lemma test_romega_0b : 
+ forall m m', 
+  0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
+Proof.
+intros m m'.
+(*omega.*)
+Admitted.
+
+Lemma test_romega_1 : 
+ forall (z z1 z2 : Z), 
+    z2 <= z1 ->
+    z1 <= z2 ->
+    z1 >= 0 ->
+    z2 >= 0 ->
+    z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
+    z >= 0.
+Proof.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_1b : 
+ forall (z z1 z2 : Z), 
+    z2 <= z1 ->
+    z1 <= z2 ->
+    z1 >= 0 ->
+    z2 >= 0 ->
+    z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
+    z >= 0.
+Proof.
+intros z z1 z2.
+omega.
+Qed.
+
+Lemma test_romega_2 : forall a b c:Z, 
+ 0<=a-b<=1 -> b-c<=2 -> a-c<=3.
+Proof.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_2b : forall a b c:Z, 
+ 0<=a-b<=1 -> b-c<=2 -> a-c<=3.
+Proof.
+intros a b c.
+omega.
+Qed.
+
+Lemma test_romega_3 : forall a b h hl hr ha hb, 
+ 0 <= ha - hl <= 1 -> 
+ -2 <= hl - hr <= 2 ->
+ h =b+1 ->
+ (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
+ (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
+ (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
+ (-2 <= ha-hr <=2 -> hb = a  + 1) -> 
+ 0 <= hb - h <= 1.
+Proof.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_3b : forall a b h hl hr ha hb, 
+ 0 <= ha - hl <= 1 -> 
+ -2 <= hl - hr <= 2 ->
+ h =b+1 ->
+ (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
+ (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
+ (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
+ (-2 <= ha-hr <=2 -> hb = a  + 1) -> 
+ 0 <= hb - h <= 1.
+Proof.
+intros a b h hl hr ha hb.
+omega.
+Qed.
+
+
+Lemma test_romega_4 : forall hr ha, 
+ ha = 0 ->
+ (ha = 0 -> hr =0) -> 
+ hr = 0.
+Proof.
+intros hr ha.
+omega.
+Qed.
+
+Lemma test_romega_5 : forall hr ha, 
+ ha = 0 ->
+ (~ha = 0 \/ hr =0) -> 
+ hr = 0.
+Proof.
+intros hr ha.
+omega.
+Qed.
+
+Lemma test_romega_6 : forall z, z>=0 -> 0>z+2 -> False.
+Proof.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False.
+Proof.
+intros z.
+omega.
+Qed.
+
+Lemma test_romega_7 : forall z, 
+  0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
+Proof.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_7b : forall z, 
+  0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
+Proof.
+intros.
+omega.
+Qed.
+
+(* Magaud #240 *)
+
+Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+intros.
+omega.
+Qed.
+
+Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+intros x y.
+omega.
+Qed.
+
+
+
+
diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v
new file mode 100644
index 00000000..04b666ed
--- /dev/null
+++ b/test-suite/success/ROmega.v
@@ -0,0 +1,98 @@
+
+Require Import ZArith ROmega.
+
+(* Submitted by Xavier Urbain 18 Jan 2002 *)
+
+Lemma lem1 :
+ forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z.
+Proof.
+intros x y.
+ (*romega.*)
+Admitted.
+
+(* Proposed by Pierre Crégut *)
+
+Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z.
+intro.
+ romega.
+Qed.
+
+(* Proposed by Jean-Christophe Filliâtre *)
+
+Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z.
+Proof.
+intros.
+ (*romega.*)
+Admitted.
+
+(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
+(* internal variable and a section variable (June 2001) *)
+
+Section A.
+Variable x y : Z.
+Hypothesis H : (x > y)%Z.
+Lemma lem4 : (x > y)%Z.
+ romega.
+Qed.
+End A.
+
+(* Proposed by Yves Bertot: because a section var, L was wrongly renamed L0 *)
+(* May 2002 *)
+
+Section B.
+Variable R1 R2 S1 S2 H S : Z.
+Hypothesis I : (R1 < 0)%Z -> R2 = (R1 + (2 * S1 - 1))%Z.
+Hypothesis J : (R1 < 0)%Z -> S2 = (S1 - 1)%Z.
+Hypothesis K : (R1 >= 0)%Z -> R2 = R1.
+Hypothesis L : (R1 >= 0)%Z -> S2 = S1.
+Hypothesis M : (H <= 2 * S)%Z.
+Hypothesis N : (S < H)%Z.
+Lemma lem5 : (H > 0)%Z.
+ romega.
+Qed.
+End B.
+
+(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *)
+Lemma lem6 :
+ forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z.
+intros.
+ romega.
+Qed.
+
+(* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *)
+Require Import Omega.
+Section C.
+Parameter g : forall m : nat, m <> 0 -> Prop.
+Parameter f : forall (m : nat) (H : m <> 0), g m H.
+Variable n : nat.
+Variable ap_n : n <> 0.
+Let delta := f n ap_n.
+Lemma lem7 : n = n.
+ (*romega.*) (*ROMEGA CANT DEAL WITH NAT*)
+Admitted.
+End C.
+
+(* Problem of dependencies *)
+Require Import Omega.
+Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0.
+intros.
+(* romega.*) (*ROMEGA CANT DEAL WITH NAT*)
+Admitted.
+
+(* Bug that what caused by the use of intro_using in Omega *)
+Require Import Omega.
+Lemma lem9 :
+ forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p.
+intros.
+(* romega.*)(*ROMEGA CANT DEAL WITH NAT*) 
+Admitted.
+
+(* Check that the interpretation of mult on nat enforces its positivity *)
+(* Submitted by Hubert Thierry (bug #743) *)
+(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z"
+Require Omega.
+Lemma lem10 : (n, m : nat) (le n (plus n (mult n m))).
+Proof.
+Intros; Omega.
+Qed.
+*)
diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v
new file mode 100644
index 00000000..0efca1e1
--- /dev/null
+++ b/test-suite/success/ROmega0.v
@@ -0,0 +1,149 @@
+Require Import ZArith ROmega.
+Open Scope Z_scope.
+
+(* Pierre L: examples gathered while debugging romega. *)
+
+Lemma test_romega_0 : 
+ forall m m', 
+  0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
+Proof.
+intros.
+(*romega.*)
+Admitted.
+
+Lemma test_romega_0b : 
+ forall m m', 
+  0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
+Proof.
+intros m m'.
+(*romega.*)
+Admitted.
+
+Lemma test_romega_1 : 
+ forall (z z1 z2 : Z), 
+    z2 <= z1 ->
+    z1 <= z2 ->
+    z1 >= 0 ->
+    z2 >= 0 ->
+    z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
+    z >= 0.
+Proof.
+intros.
+romega.
+Qed.
+
+Lemma test_romega_1b : 
+ forall (z z1 z2 : Z), 
+    z2 <= z1 ->
+    z1 <= z2 ->
+    z1 >= 0 ->
+    z2 >= 0 ->
+    z1 >= z2 /\ z = z1 \/ z1 <= z2 /\ z = z2 ->
+    z >= 0.
+Proof.
+intros z z1 z2.
+(* romega. *) 
+Admitted.
+
+Lemma test_romega_2 : forall a b c:Z, 
+ 0<=a-b<=1 -> b-c<=2 -> a-c<=3.
+Proof.
+intros.
+romega.
+Qed.
+
+Lemma test_romega_2b : forall a b c:Z, 
+ 0<=a-b<=1 -> b-c<=2 -> a-c<=3.
+Proof.
+intros a b c.
+(*romega.*)
+Admitted.
+
+Lemma test_romega_3 : forall a b h hl hr ha hb, 
+ 0 <= ha - hl <= 1 -> 
+ -2 <= hl - hr <= 2 ->
+ h =b+1 ->
+ (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
+ (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
+ (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
+ (-2 <= ha-hr <=2 -> hb = a  + 1) -> 
+ 0 <= hb - h <= 1.
+Proof.
+intros.
+romega.
+Qed.
+
+Lemma test_romega_3b : forall a b h hl hr ha hb, 
+ 0 <= ha - hl <= 1 -> 
+ -2 <= hl - hr <= 2 ->
+ h =b+1 ->
+ (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) ->
+ (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) ->
+ (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) ->
+ (-2 <= ha-hr <=2 -> hb = a  + 1) -> 
+ 0 <= hb - h <= 1.
+Proof.
+intros a b h hl hr ha hb.
+romega.
+Qed.
+
+
+Lemma test_romega_4 : forall hr ha, 
+ ha = 0 ->
+ (ha = 0 -> hr =0) -> 
+ hr = 0.
+Proof.
+intros hr ha.
+romega.
+Qed.
+
+Lemma test_romega_5 : forall hr ha, 
+ ha = 0 ->
+ (~ha = 0 \/ hr =0) -> 
+ hr = 0.
+Proof.
+intros hr ha.
+romega.
+Qed.
+
+Lemma test_romega_6 : forall z, z>=0 -> 0>z+2 -> False.
+Proof.
+intros.
+romega.
+Qed.
+
+Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False.
+Proof.
+intros z.
+(*romega. *)
+Admitted.
+
+Lemma test_romega_7 : forall z, 
+  0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
+Proof.
+intros.
+(*romega.*)
+Admitted.
+
+Lemma test_romega_7b : forall z, 
+  0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
+Proof.
+intros.
+(*romega.*)
+Admitted.
+
+(* Magaud #240 *)
+
+Lemma test_romega_8 : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+intros.
+romega.
+Qed.
+
+Lemma test_romega_8b : forall x y:Z, x*x<y*y-> ~ y*y <= x*x.
+intros x y.
+romega.
+Qed.
+
+
+
+
diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v
new file mode 100644
index 00000000..9d47c9f6
--- /dev/null
+++ b/test-suite/success/ROmega2.v
@@ -0,0 +1,28 @@
+Require Import ZArith ROmega.
+
+(* Submitted by Yegor Bryukhov (#922) *)
+
+Open Scope Z_scope.
+
+Lemma Test46 : 
+forall v1 v2 v3 v4 v5 : Z,
+((2 * v4) + (5)) + (8 * v2) <= ((4 * v4) + (3 * v4)) + (5 * v4) ->
+9 * v4 > (1 * v4) + ((2 * v1) + (0 * v2)) ->
+((9 * v3) + (2 * v5)) + (5 * v2) = 3 * v4 ->
+0 > 6 * v1 ->
+(0 * v3) + (6 * v2) <> 2 ->
+(0 * v3) + (5 * v5) <> ((4 * v2) + (8 * v2)) + (2 * v5) ->
+7 * v3 > 5 * v5 ->
+0 * v4 >= ((5 * v1) + (4 * v1)) + ((6 * v5) + (3 * v5)) ->
+7 * v2 = ((3 * v2) + (6 * v5)) + (7 * v2) ->
+0 * v3 > 7 * v1 ->
+9 * v2 < 9 * v5 ->
+(2 * v3) + (8 * v1) <= 5 * v4 ->
+5 * v2 = ((5 * v1) + (0 * v5)) + (1 * v2) ->
+0 * v5 <= 9 * v2 ->
+((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9))
+-> False.
+intros.
+(*romega.*)
+Admitted.
+
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index d79b85df..60e170e4 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -1011,7 +1011,7 @@ Implicit Arguments Vnil [A].
 Implicit Arguments Vhead [A n].
 Implicit Arguments Vtail [A n].
 
-Definition Vid : forall (A : Set)(n:nat), vector A n -> vector A n.
+Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n.
 Proof.
  destruct n; intro v.
  exact Vnil.
@@ -1024,7 +1024,7 @@ Eval simpl in (fun (A:Set)(v:vector A 0) => v).
 
 
 
-Lemma Vid_eq : forall (n:nat) (A:Set)(v:vector A n), v=(Vid _ n v).
+Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
 Proof.
  destruct v. 
  reflexivity.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index ede573a3..9f938e10 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -1,3 +1,17 @@
+(* Submitted by Robert Schneck *)
+
+Parameter A B C D : Prop.
+Axiom X : A -> B -> C /\ D.
+
+Lemma foo : A -> B -> C.
+Proof.
+intros. 
+destruct X. (* Should find axiom X and should handle arguments of X *)
+assumption.
+assumption.
+assumption.
+Qed.
+
 (* Simplification of bug 711 *)
 
 Parameter f : true = false.
@@ -7,3 +21,5 @@ set (b := true) in *.
 (* Check that it doesn't fail with an anomaly *)
 (* Ultimately, adapt destruct to make it succeeding *)
 try destruct b.
+Abort.
+
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 64875fba..baeec147 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -59,7 +59,7 @@ Check
 
 (* Check instantiation of nested evars (bug #1089) *)
 
-Check (fun f:(forall (v:Set->Set), v (v nat) -> nat) => f _ (Some (Some O))).
+Check (fun f:(forall (v:Type->Type), v (v nat) -> nat) => f _ (Some (Some O))).
 
 (* This used to fail with anomaly "evar was not declared" in V8.0pl3 *)
 
diff --git a/test-suite/success/if.v b/test-suite/success/if.v
index 3f763863..9fde95e8 100644
--- a/test-suite/success/if.v
+++ b/test-suite/success/if.v
@@ -3,3 +3,10 @@
 
 Check (fun b : bool => if b then Type else nat).
 
+(* Check correct use of if-then-else predicate annotation (cf bug 690) *)
+
+Check fun b : bool =>
+ if b as b0 return (if b0 then b0 = true else b0 = false)
+ then refl_equal true
+ else refl_equal false.
+
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index b61cf275..4346ce9a 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -64,3 +64,26 @@ intro P.
  refine (P _ _).
 reflexivity.
 Abort.
+
+(* Submitted by Jacek Chrzaszcz (bug #1102) *)
+
+(* le probl�me a �t� r�solu ici par normalisation des evars pr�sentes
+   dans les types d'evars, mais le probl�me reste a priori ouvert dans
+   le cas plus g�n�ral d'evars non instanci�es dans les types d'autres
+   evars *)
+
+Goal exists n:nat, n=n.
+refine (ex_intro _ _ _).
+Abort.
+
+(* Used to failed with error not clean *)
+
+Definition div :
+  forall x:nat, (forall y:nat, forall n:nat, {q:nat | y = q*n}) -> 
+     forall n:nat, {q:nat | x = q*n}.
+refine
+  (fun m div_rec n =>
+     match div_rec m n with
+     | exist _ _ => _
+     end).
+Abort.
diff --git a/test-suite/success/unicode_utf8.v b/test-suite/success/unicode_utf8.v
index e3c4dd30..19e306fe 100644
--- a/test-suite/success/unicode_utf8.v
+++ b/test-suite/success/unicode_utf8.v
@@ -4,6 +4,9 @@
 
 (* Check Greek letters *)
 Definition test_greek : nat -> nat := fun Δ => Δ.
+Parameter ℝ : Set.
+Parameter π : ℝ.
 
 (* Check indices *)
 Definition test_indices : nat -> nat := fun x₁ => x₁.
+Definition π₂ := snd.