From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 8 May 2013 17:47:10 +0200
Subject: Imported Upstream version 8.4pl2dfsg

---
 test-suite/bugs/closed/2955.v               | 52 +++++++++++++++++++++++++++++
 test-suite/bugs/closed/shouldsucceed/2629.v | 22 ++++++++++++
 test-suite/bugs/closed/shouldsucceed/2668.v |  6 ++++
 test-suite/bugs/closed/shouldsucceed/2734.v | 15 +++++++++
 test-suite/bugs/closed/shouldsucceed/2750.v | 23 +++++++++++++
 test-suite/bugs/closed/shouldsucceed/2928.v | 11 ++++++
 test-suite/bugs/closed/shouldsucceed/2983.v |  8 +++++
 test-suite/bugs/closed/shouldsucceed/2995.v |  9 +++++
 test-suite/bugs/closed/shouldsucceed/3000.v |  2 ++
 test-suite/bugs/closed/shouldsucceed/3004.v |  7 ++++
 test-suite/bugs/closed/shouldsucceed/3008.v | 29 ++++++++++++++++
 test-suite/output/inference.out             |  4 +++
 test-suite/output/inference.v               | 12 +++++++
 test-suite/success/remember.v               |  8 +++++
 14 files changed, 208 insertions(+)
 create mode 100644 test-suite/bugs/closed/2955.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2629.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2668.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2734.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2750.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2928.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2983.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2995.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/3000.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/3004.v
 create mode 100644 test-suite/bugs/closed/shouldsucceed/3008.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/2955.v b/test-suite/bugs/closed/2955.v
new file mode 100644
index 00000000..45e24b5f
--- /dev/null
+++ b/test-suite/bugs/closed/2955.v
@@ -0,0 +1,52 @@
+Require Import Coq.Arith.Arith.
+
+Module A.
+
+  Fixpoint foo (n:nat) :=
+  match n with
+  | 0 => 0
+  | S n => bar n
+  end
+
+  with bar (n:nat) :=
+  match n with
+  | 0 => 0
+  | S n => foo n
+  end.
+
+  Lemma using_foo:
+    forall (n:nat), foo n = 0 /\ bar n = 0.
+  Proof.
+    induction n ; split ; auto ;
+    destruct IHn ; auto.
+  Qed.
+
+End A.
+
+
+Module B.
+  
+  Module A := A.
+  Import A.
+
+End B.
+
+Module E.
+
+  Module B := B.
+  Import B.A.
+
+  (* Bug 1 *)
+  Lemma test_1:
+    forall (n:nat), foo n = 0.
+  Proof.
+    intros ; destruct n.
+    reflexivity.
+    specialize (A.using_foo (S n)) ; intros.
+    simpl in H.
+    simpl.
+    destruct H.
+    assumption.
+  Qed.
+
+End E.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2629.v b/test-suite/bugs/closed/shouldsucceed/2629.v
new file mode 100644
index 00000000..759cd3dd
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2629.v
@@ -0,0 +1,22 @@
+Class Join (t: Type) : Type := mkJoin {join: t -> t -> t -> Prop}.
+
+Class sepalg (t: Type) {JOIN: Join t} : Type :=
+  SepAlg   {
+   join_eq: forall {x y z z'}, join x y z -> join x y z' -> z = z';
+   join_assoc: forall {a b c d e}, join a b d -> join d c e ->
+                    {f : t & join b c f /\ join a f e};
+   join_com: forall {a b c}, join a b c -> join b a c;
+   join_canc: forall {a1 a2 b c}, join a1 b c -> join a2 b c -> a1=a2;
+
+   unit_for : t -> t -> Prop := fun e a => join e a a;
+   join_ex_units: forall a, {e : t & unit_for e a}
+}.
+
+Definition joins {A} `{Join A} (a b : A) : Prop :=
+ exists c, join a b c.
+
+Lemma join_joins {A} `{sepalg A}: forall {a b c},
+ join a b c -> joins a b.
+Proof.
+ firstorder.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2668.v b/test-suite/bugs/closed/shouldsucceed/2668.v
new file mode 100644
index 00000000..74c8fa34
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2668.v
@@ -0,0 +1,6 @@
+Require Import MSetPositive.
+Require Import MSetProperties.
+
+Module Pos := MSetPositive.PositiveSet.
+Module PPPP := MSetProperties.WPropertiesOn(Pos).
+Print Module PPPP.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2734.v b/test-suite/bugs/closed/shouldsucceed/2734.v
new file mode 100644
index 00000000..826361be
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2734.v
@@ -0,0 +1,15 @@
+Require Import Arith List.
+Require Import OrderedTypeEx.
+
+Module Adr.
+ Include Nat_as_OT.
+ Definition nat2t (i: nat) : t := i.
+End Adr.
+
+Inductive expr :=  Const: Adr.t -> expr.
+
+Inductive control := Go: expr ->  control.
+
+Definition program :=  (Adr.t * (control))%type.
+
+Fail Definition myprog : program := (Adr.nat2t 0,   Go (Adr.nat2t 0) ).
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2750.v b/test-suite/bugs/closed/shouldsucceed/2750.v
new file mode 100644
index 00000000..fc580f10
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2750.v
@@ -0,0 +1,23 @@
+
+Module Type ModWithRecord.
+
+  Record foo : Type :=
+  { A : nat
+  ; B : nat
+  }.
+End ModWithRecord.
+
+Module Test_ModWithRecord (M : ModWithRecord).
+
+  Definition test1 : M.foo :=
+    {| M.A := 0
+     ; M.B := 2
+     |}.
+
+  Module B := M.
+
+  Definition test2 : M.foo :=
+    {| M.A := 0
+     ; M.B := 2
+     |}.
+End Test_ModWithRecord.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2928.v b/test-suite/bugs/closed/shouldsucceed/2928.v
new file mode 100644
index 00000000..21e92ae2
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2928.v
@@ -0,0 +1,11 @@
+Class Equiv A := equiv: A -> A -> Prop.
+Infix "=" := equiv : type_scope.
+
+Class Associative {A} f `{Equiv A} := associativity x y z : f x (f y z) = f (f x y) z.
+
+Class SemiGroup A op `{Equiv A} := { sg_ass :>> Associative op }.
+
+Class SemiLattice A op `{Equiv A} :=
+    { semilattice_sg :>> SemiGroup A op
+    ; redundant : Associative op
+    }.
diff --git a/test-suite/bugs/closed/shouldsucceed/2983.v b/test-suite/bugs/closed/shouldsucceed/2983.v
new file mode 100644
index 00000000..15598352
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2983.v
@@ -0,0 +1,8 @@
+Module Type ModA.
+End ModA.
+Module Type ModB(A : ModA).
+End ModB.
+Module Foo(A : ModA)(B : ModB A).
+End Foo.
+
+Print Module Foo.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2995.v b/test-suite/bugs/closed/shouldsucceed/2995.v
new file mode 100644
index 00000000..ba3acd08
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2995.v
@@ -0,0 +1,9 @@
+Module Type Interface.
+  Parameter error: nat.
+End Interface.
+
+Module Implementation <: Interface.
+  Definition t := bool.
+  Definition error: t := false.
+Fail End Implementation.
+(* A UserError here is expected, not an uncaught Not_found *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/3000.v b/test-suite/bugs/closed/shouldsucceed/3000.v
new file mode 100644
index 00000000..27de34ed
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/3000.v
@@ -0,0 +1,2 @@
+Inductive t (t':Type) : Type := A | B.
+Definition d := match t with _ => 1 end. (* used to fail on list_chop *)
diff --git a/test-suite/bugs/closed/shouldsucceed/3004.v b/test-suite/bugs/closed/shouldsucceed/3004.v
new file mode 100644
index 00000000..896b1958
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/3004.v
@@ -0,0 +1,7 @@
+Set Implicit Arguments.
+Unset Strict Implicit.
+Parameter (M : nat -> Type).
+Parameter (mp : forall (T1 T2 : Type) (f : T1 -> T2), list T1 -> list T2).
+
+Definition foo (s : list {n : nat & M n}) :=
+  let exT := existT in mp (fun x => projT1 x) s.
diff --git a/test-suite/bugs/closed/shouldsucceed/3008.v b/test-suite/bugs/closed/shouldsucceed/3008.v
new file mode 100644
index 00000000..3f3a979a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/3008.v
@@ -0,0 +1,29 @@
+Module Type Intf1.
+Parameter T : Type.
+Inductive a := A.
+End Intf1.
+
+Module Impl1 <: Intf1.
+Definition T := unit.
+Inductive a := A.
+End Impl1.
+
+Module Type Intf2
+  (Impl1 : Intf1).
+Parameter x : Impl1.A=Impl1.A -> Impl1.T.
+End Intf2.
+
+Module Type Intf3
+  (Impl1 : Intf1)
+  (Impl2 : Intf2(Impl1)).
+End Intf3.
+
+Fail Module Toto
+  (Impl1' : Intf1)
+  (Impl2 : Intf2(Impl1'))
+  (Impl3 : Intf3(Impl1)(Impl2)).
+(* A UserError is expected here, not an uncaught Not_found *)
+
+(* NB : the Inductive above and the A=A weren't in the initial test,
+   they are here only to force an access to the environment
+   (cf [Printer.qualid_of_global]) and check that this env is ok. *)
\ No newline at end of file
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index bca3b361..4f8de1dc 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -4,3 +4,7 @@ fun e : option L => match e with
                     | None => None
                     end
      : option L -> option L
+fun n : nat => let x := A n in ?12 ?15:T n
+     : forall n : nat, T n
+fun n : nat => ?20 ?23:T n
+     : forall n : nat, T n
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index 968ea71a..2b564f48 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -12,3 +12,15 @@ Definition P (e:option L) :=
   end.
 
 Print P.
+
+(* Check that the heuristic to solve constraints is not artificially
+   dependent on the presence of a let-in, and in particular that the
+   second [_] below is not inferred to be n, as if obtained by
+   first-order unification with [T n] of the conclusion [T _] of the
+   type of the first [_]. *)
+
+(* Note: exact numbers of evars are not important... *)
+
+Inductive T (n:nat) : Type := A : T n.
+Check fun n (x:=A n:T n) => _ _ : T n.
+Check fun n => _ _ : T n.
diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
index 5f8ed03d..0befe054 100644
--- a/test-suite/success/remember.v
+++ b/test-suite/success/remember.v
@@ -6,3 +6,11 @@ Fail remember nat as X.
 Fail remember nat as X in H. (* This line used to succeed in 8.3 *)
 Fail remember nat as X.
 Abort.
+
+(* Testing Ltac interpretation of remember (was not working up to r16181) *)
+
+Goal (1 + 2 + 3 = 6).
+let name := fresh "fresh" in
+remember (1 + 2) as x eqn:name.
+rewrite fresh.
+Abort.
-- 
cgit v1.2.3