Merge branch 'v8.5'

9 files changed, 61 insertions, 3 deletions

diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v
index 9e12b990b7..049589325e 100644
--- a/test-suite/bugs/closed/3309.v
+++ b/test-suite/bugs/closed/3309.v
@@ -315,8 +315,6 @@ Definition abmonoidfracrel ( X : abmonoid ) ( A : @submonoids X ) :  hrel (@setq
 intros; exact (@quotrel _ _).
 Defined.
 
-(* Unset Kernel Term Sharing. *)
-
 Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit.
 
 Definition ispartlbinopabmonoidfracrel_type : Type :=
@@ -326,3 +324,10 @@ Definition ispartlbinopabmonoidfracrel_type : Type :=
 Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in
                                       ispartlbinopabmonoidfracrel_type in exact t)$.
 
+Unset Kernel Term Sharing.
+
+Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit.
+
+Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in
+                                      ispartlbinopabmonoidfracrel_type in exact t)$.
+
diff --git a/test-suite/bugs/opened/3490.v b/test-suite/bugs/closed/3490.v
index e7a5caa1de..e7a5caa1de 100644
--- a/test-suite/bugs/opened/3490.v
+++ b/test-suite/bugs/closed/3490.v
diff --git a/test-suite/bugs/closed/3755.v b/test-suite/bugs/closed/3755.v
new file mode 100644
index 0000000000..77427ace58
--- /dev/null
+++ b/test-suite/bugs/closed/3755.v
@@ -0,0 +1,16 @@
+(* File reduced by coq-bug-finder from original input, then from 6729 lines to 
+411 lines, then from 148 lines to 115 lines, then from 99 lines to 70 lines, 
+then from 85 lines to 63 lines, then from 76 lines to 55 lines, then from 61 
+lines to 17 lines *)
+(* coqc version trunk (January 2015) compiled on Jan 17 2015 21:58:5 with OCaml 
+4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk 
+(9e6b28c04ad98369a012faf3bd4d630cf123a473) *)
+Set Printing Universes.
+Section param.
+  Variable typeD : Set -> Set.
+  Variable STex : forall (T : Type) (p : T -> Set), Set.
+  Definition existsEach_cons' v (P : @sigT _ typeD -> Set) :=
+    @STex _ (fun x => P (@existT _ _ v x)).
+
+  Check @existT _ _ STex STex.
diff --git a/test-suite/bugs/closed/3808.v b/test-suite/bugs/closed/3808.v
new file mode 100644
index 0000000000..6e19ddf8dc
--- /dev/null
+++ b/test-suite/bugs/closed/3808.v
@@ -0,0 +1,2 @@
+Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i})
+  := foo : Foo.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3916.v b/test-suite/bugs/closed/3916.v
new file mode 100644
index 0000000000..55c3a35c3a
--- /dev/null
+++ b/test-suite/bugs/closed/3916.v
@@ -0,0 +1,3 @@
+Require Import List.
+Fail Hint Resolve -> in_map.
+
diff --git a/test-suite/bugs/closed/4016.v b/test-suite/bugs/closed/4016.v
new file mode 100644
index 0000000000..41cb1a8884
--- /dev/null
+++ b/test-suite/bugs/closed/4016.v
@@ -0,0 +1,12 @@
+Require Import Setoid.
+
+Parameter eq : relation nat.
+Declare Instance Equivalence_eq : Equivalence eq.
+
+Lemma foo : forall z, eq z 0 -> forall x, eq x 0 -> eq z x.
+Proof.
+intros z Hz x Hx.
+rewrite <- Hx in Hz.
+destruct z.
+Abort.
+
diff --git a/test-suite/bugs/closed/4017.v b/test-suite/bugs/closed/4017.v
index a6f177b496..aa810f4f0e 100644
--- a/test-suite/bugs/closed/4017.v
+++ b/test-suite/bugs/closed/4017.v
@@ -1,3 +1,5 @@
+Set Implicit Arguments.
+
 (* Use of implicit arguments was lost in multiple variable declarations *)
 Variables 
   (A1 : Type)
diff --git a/test-suite/bugs/closed/4018.v b/test-suite/bugs/closed/4018.v
index c3a045943c..8895e09e02 100644
--- a/test-suite/bugs/closed/4018.v
+++ b/test-suite/bugs/closed/4018.v
@@ -1,3 +1,3 @@
 (* Catching PatternMatchingFailure was lost at some point *)
 Goal nat -> True.
-intros [=].
+Fail intros [=].
diff --git a/test-suite/success/qed_export.v b/test-suite/success/qed_export.v
new file mode 100644
index 0000000000..ee84cb94e9
--- /dev/null
+++ b/test-suite/success/qed_export.v
@@ -0,0 +1,18 @@
+Lemma a : True.
+Proof.
+assert True as H.
+  abstract (trivial) using exported_seff.
+exact H.
+Fail Qed export a_subproof.
+Qed export exported_seff.
+Check ( exported_seff : True ).
+
+Lemma b : True.
+Proof.
+assert True as H.
+  abstract (trivial) using exported_seff2.
+exact H.
+Qed.
+
+Fail Check ( exported_seff2 : True ).
+