Imported Upstream version 8.0pl3+8.1beta.2upstream/8.0pl3+8.1beta.2

7 files changed, 97 insertions, 12 deletions

diff --git a/test-suite/failure/inductive1.v b/test-suite/failure/inductive1.v
new file mode 100644
index 00000000..3b57d919
--- /dev/null
+++ b/test-suite/failure/inductive1.v
@@ -0,0 +1,4 @@
+(* A check that sort-polymorphic product is not set too low *)
+
+Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
+Check (fun (A:Type) (B:Prop) => (prod A B : Prop)).
diff --git a/test-suite/failure/inductive2.v b/test-suite/failure/inductive2.v
new file mode 100644
index 00000000..b77474be
--- /dev/null
+++ b/test-suite/failure/inductive2.v
@@ -0,0 +1,4 @@
+(* A check that sort-polymorphic product is not set too low *)
+
+Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
+Check (fun (A:Prop) (B:Type) => (prod A B : Prop)).
diff --git a/test-suite/failure/inductive3.v b/test-suite/failure/inductive3.v
new file mode 100644
index 00000000..e5a4e1b6
--- /dev/null
+++ b/test-suite/failure/inductive3.v
@@ -0,0 +1,5 @@
+(* Check that the nested inductive types positivity check avoids recursively 
+   non uniform parameters (at least if these parameters break positivity) *)
+
+Inductive t (A:Type) : Type := c : t (A -> A) -> t A.
+Inductive u : Type := d : u | e : t u -> u.
diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
new file mode 100644
index 00000000..003810cc
--- /dev/null
+++ b/test-suite/success/CanonicalStructure.v
@@ -0,0 +1,7 @@
+(* Bug #1172 *)
+
+Structure foo : Type := Foo {
+   A : Set; Aopt := option A; unopt : Aopt -> A
+}.
+
+Canonical Structure unopt_nat := @Foo nat (fun _ => O).
diff --git a/test-suite/success/Case18.v b/test-suite/success/Case18.v
index a57fe413..91c80e88 100644
--- a/test-suite/success/Case18.v
+++ b/test-suite/success/Case18.v
@@ -3,9 +3,12 @@
 Definition g x :=
   match x with ((((1 as x),_) | (_,x)), (_,(2 as y))|(y,_)) => (x,y) end.
 
-Eval compute in (g ((1,2),(3,4))).
-(* (1,3) *)
+Check (refl_equal _ : g ((1,2),(3,4)) = (1,3)).
 
-Eval compute in (g ((1,4),(3,2))).
-(* (1,2) *)
+Check (refl_equal _ : g ((1,4),(3,2)) = (1,2)).
 
+Fixpoint max (n m:nat) {struct m} : nat :=
+  match  n, m with
+  | S n', S m' => S (max n' m')
+  | 0, p | p, 0 => p
+  end.
diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v
new file mode 100644
index 00000000..9a6ed71a
--- /dev/null
+++ b/test-suite/success/Case19.v
@@ -0,0 +1,8 @@
+(* This used to fail in Coq version 8.1 beta due to a non variable
+   universe (issued by the inductive sort-polymorphism) being sent by
+   pretyping to the kernel (bug #1182) *)
+
+Variable T : Type.
+Variable x : nat*nat.
+
+Check let (_, _) := x in sigT (fun _ : T => nat).
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index 939d06c7..1c3e56f2 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -29,6 +29,18 @@ intros n m.
  functional induction ftest n m; auto.
 Qed.
 
+Lemma test2 : forall m n, ~ 2 = ftest n m.
+Proof. 
+intros n m;intro H.
+functional inversion H ftest.
+Qed.
+
+Lemma test3 : forall n m, ftest n m = 0 -> (n = 0 /\ m = 0)  \/ n <> 0.
+Proof.
+functional inversion 1 ftest;auto.
+Qed.
+
+
 Require Import Arith.
 Lemma test11 : forall m : nat, ftest 0 m <= 2.
 intros m.
@@ -112,7 +124,8 @@ Function iseven (n : nat) : bool :=
   | S (S m) => iseven m
   | _ => false
   end.
- 
+
+
 Function funex (n : nat) : nat :=
   match iseven n with
   | true => n
@@ -122,6 +135,7 @@ Function funex (n : nat) : nat :=
              end
   end.
  
+
 Function nat_equal_bool (n m : nat) {struct n} : bool :=
   match n with
   | O => match m with
@@ -151,7 +165,6 @@ Qed.
 
 (* reuse this lemma as a scheme:*)
 
-
 Function nested_lam (n : nat) : nat -> nat :=
   match n with
   | O => fun m : nat => 0
@@ -184,7 +197,6 @@ auto with arith.
  auto with arith.
 Qed.
 
- 
 Function plus_x_not_five'' (n m : nat) {struct n} : nat :=
   let x := nat_equal_bool m 5 in
   let y := 0 in
@@ -206,7 +218,7 @@ Qed.
 Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true.
 intros n m.
  functional induction nat_equal_bool n m; simpl in |- *; intros hyp; auto.
-rewrite <- hyp in H1; simpl in H1;tauto. 
+rewrite <- hyp in y; simpl in y;tauto. 
 inversion hyp.
 Qed.
  
@@ -280,14 +292,14 @@ destruct n. tauto.
 destruct n. inversion istr.
 destruct n. inversion istr.
 destruct n. tauto.
-simpl in *. inversion H1.
+simpl in *. inversion H0.
 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.
+rewrite H in y; simpl in y;tauto.
 Qed.
  
 Function ftest4 (n m : nat) : nat :=
@@ -353,7 +365,7 @@ Function ftest2 (n m : nat) {struct n} : nat :=
   | S p => ftest2 p m
   end.
  
-Lemma test2 : forall n m : nat, ftest2 n m <= 2.
+Lemma test2' : forall n m : nat, ftest2 n m <= 2.
 intros n m.
  functional induction ftest2 n m; simpl in |- *; intros; auto.
 Qed.
@@ -367,7 +379,7 @@ Function ftest3 (n m : nat) {struct n} : nat :=
            end
   end.
  
-Lemma test3 : forall n m : nat, ftest3 n m <= 2.
+Lemma test3' : forall n m : nat, ftest3 n m <= 2.
 intros n m.
  functional induction ftest3 n m.
 intros.
@@ -442,10 +454,52 @@ intros n m.
  functional induction ftest6 n m; simpl in |- *; auto.
 Qed.
 
+(* Some tests with modules *) 
+Module M.
+Function test_m (n:nat) : nat := 
+  match n with 
+    | 0 => 0
+    | S n =>  S (S (test_m n))
+  end.
 
+Lemma test_m_is_double :  forall n, div2 (test_m n) = n.
+Proof.
+intros n.
+functional induction (test_m n).
+reflexivity.
+simpl;rewrite IHn0;reflexivity.
+Qed.
+End M.
+(* We redefine a new Function with the same name *) 
+Function test_m (n:nat) : nat := 
+  pred n.
+
+Lemma test_m_is_pred : forall n, test_m n = pred n.
+Proof. 
+intro n.
+functional induction (test_m n). (* the test_m_ind to use is the last defined  saying that test_m = pred*) 
+reflexivity.
+Qed.
 
+(* Checks if the dot notation are correctly treated in infos *)
+Lemma M_test_m_is_double : forall n, div2 (M.test_m n) = n.
+intro n.
+(* here we should apply M.test_m_ind *)
+functional induction (M.test_m n).
+reflexivity.
+simpl;rewrite IHn0;reflexivity.
+Qed.
 
+Import M.
+(* Now test_m is the one which defines double *)
 
+Lemma test_m_is_double : forall n, div2 (M.test_m n) = n.
+intro n.
+(* here we should apply M.test_m_ind *)
+functional induction (test_m n).
+reflexivity.
+simpl;rewrite IHn0;reflexivity.
+Qed.