Merge branch 'v8.5'

9 files changed, 153 insertions, 11 deletions

diff --git a/test-suite/bugs/closed/2590.v b/test-suite/bugs/closed/2590.v
new file mode 100644
index 0000000000..e594e96936
--- /dev/null
+++ b/test-suite/bugs/closed/2590.v
@@ -0,0 +1,19 @@
+Require Import Relation_Definitions RelationClasses Setoid SetoidClass.
+
+Section Bug.
+
+  Context {A : Type} (R : relation A).
+  Hypothesis pre : PreOrder R.
+  Context `{SA : Setoid A}.
+
+  Goal True.
+  set (SA' := SA).
+    assert ( forall SA0 : Setoid A,
+               @PartialOrder A (@equiv A SA0) (@setoid_equiv A SA0) R pre ).
+    rename SA into SA0.
+    intro SA.
+    admit.
+    admit.
+Qed.
+End Bug.
+
diff --git a/test-suite/bugs/closed/2775.v b/test-suite/bugs/closed/2775.v
new file mode 100644
index 0000000000..f1f384bdf7
--- /dev/null
+++ b/test-suite/bugs/closed/2775.v
@@ -0,0 +1,6 @@
+Inductive typ : forall (T:Type), list T ->  Type -> Prop :=
+  | Get : forall (T:Type) (l:list T), typ T l T.
+
+
+Derive Inversion inv with 
+(forall (X: Type) (y: list nat), typ nat y X)  Sort Prop.
diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v
index fcebdec728..9e12b990b7 100644
--- a/test-suite/bugs/closed/3309.v
+++ b/test-suite/bugs/closed/3309.v
@@ -315,12 +315,14 @@ 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 :=
   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
+Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in
                                       ispartlbinopabmonoidfracrel_type in exact t)$.
 
diff --git a/test-suite/bugs/closed/3560.v b/test-suite/bugs/closed/3560.v
new file mode 100644
index 0000000000..65ce4fb6b0
--- /dev/null
+++ b/test-suite/bugs/closed/3560.v
@@ -0,0 +1,15 @@
+
+(* File reduced by coq-bug-finder from original input, then from 6236 lines to 1049 lines, then from 920 lines to 209 lines, then from 179 lines to 30 lines *)
+(* coqc version trunk (August 2014) compiled on Aug 31 2014 10:12:32 with OCaml 4.01.0
+   coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (437b91a3ffd7327975a129b95b24d3f66ad7f3e4) *)
+
+Set Primitive Projections.
+Set Implicit Arguments.
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+Notation "x * y" := (prod x y) : type_scope.
+Record Equiv A B := { equiv_fun :> A -> B ; equiv_isequiv : forall P, P equiv_fun }.
+Goal forall (A B : Type) (C : Type), Equiv (A -> B -> C) (A * B -> C).
+Proof.
+  intros.
+  exists (fun u => fun x => u (fst x) (snd x)).
+Abort.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3783.v b/test-suite/bugs/closed/3783.v
new file mode 100644
index 0000000000..33ca9651a5
--- /dev/null
+++ b/test-suite/bugs/closed/3783.v
@@ -0,0 +1,32 @@
+Fixpoint exp (n : nat) (T : Set)
+  := match n with
+       | 0 => T
+       | S n' => exp n' (T * T)
+     end.
+Definition big := Eval compute in exp 13 nat.
+Module NonPrim.
+  Unset Primitive Projections.
+  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+  Definition x : sigT (fun x => x).
+  Proof.
+    exists big; admit.
+  Defined.
+  Goal True.
+    pose ((fun y => y = y) (projT1 _ x)) as y.
+    Time cbv beta in y. (* 0s *)
+    admit.
+  Defined.
+End NonPrim.
+Module Prim.
+  Set Primitive Projections.
+  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+  Definition x : sigT (fun x => x).
+  Proof.
+    exists big; admit.
+  Defined.
+  Goal True.
+    pose ((fun y => y = y) (projT1 _ x)) as y.
+    Timeout 1 cbv beta in y. (* takes around 2s.  Grows with the value passed to [exp] above *)
+    admit.
+  Defined.
+End Prim.
\ No newline at end of file
diff --git a/test-suite/bugs/opened/3786.v b/test-suite/bugs/closed/3786.v
index 5a1241151c..fd3bd7bd76 100644
--- a/test-suite/bugs/opened/3786.v
+++ b/test-suite/bugs/closed/3786.v
@@ -26,15 +26,7 @@ Definition sumUniqueImpl (ls : list nat)
 Proof.
   eexists.
   match goal with
-    | [ |- refine ?a ?b ] => let a' := eval hnf in a in refine (_ : refine a' b)
-  end;
-  try setoid_rewrite (@finite_set_handle_cardinal).
-  Undo.
-  match goal with
     | [ |- refine ?a ?b ] => let a' := eval hnf in a in change (refine a' b)
   end.
-  try setoid_rewrite (@finite_set_handle_cardinal). (* Anomaly: Uncaught exception Invalid_argument("decomp_pointwise").
-Please report. *)
-  instantiate (1 := admit).
-  admit.
-Defined.
+  try setoid_rewrite (@finite_set_handle_cardinal).
+Abort.
diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v
new file mode 100644
index 0000000000..7c3cc6b791
--- /dev/null
+++ b/test-suite/bugs/closed/3881.v
@@ -0,0 +1,35 @@
+(* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 2236 lines to 1877 lines, then from 1652 lines to 160 lines, then from 102 lines to 34 lines *)
+(* coqc version trunk (December 2014) compiled on Dec 23 2014 22:6:43 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (90ed6636dea41486ddf2cc0daead83f9f0788163) *)
+Generalizable All Variables.
+Require Import Coq.Init.Notations.
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+Axiom admit : forall {T}, T.
+Notation "g 'o' f" := (fun x => g (f x)) (at level 40, left associativity).
+Notation "g 'o' f" := $(let g' := g in let f' := f in exact (fun x => g' (f' x)))$ (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *)
+Inductive eq {A} (x:A) : A -> Prop := eq_refl : x = x where "x = y" := (@eq _ x y) : type_scope.
+Arguments eq_refl {_ _}.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with eq_refl => eq_refl end.
+Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A ; eisretr : forall x, f (equiv_inv x) = x }.
+Arguments eisretr {A B} f {_} _.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'").
+Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (g o f) | 1000 := admit.
+Definition isequiv_homotopic {A B} (f : A -> B) (g : A -> B) `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g := admit.
+Global Instance isequiv_inverse {A B} (f : A -> B) {feq : IsEquiv f} : IsEquiv f^-1 | 10000 := admit.
+Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C} `{IsEquiv A B f} `{IsEquiv A C (g o f)} : IsEquiv g.
+Proof.
+  pose (fun H => @isequiv_homotopic _ _ ((g o f) o f^-1) _ H
+                                    (fun b => ap g (eisretr f b))) as k.
+  revert k.
+  let x := match goal with |- let k := ?x in _ => constr:x end in
+  intro k; clear k;
+  pose (x _).
+  pose (@isequiv_homotopic _ _ ((g o f) o f^-1) g _
+                           (fun b => ap g (eisretr f b))).
+  Undo. 
+  apply (@isequiv_homotopic _ _ ((g o f) o f^-1) g _
+                           (fun b => ap g (eisretr f b))).
+Qed.
+  
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3978.v b/test-suite/bugs/closed/3978.v
new file mode 100644
index 0000000000..26e021e719
--- /dev/null
+++ b/test-suite/bugs/closed/3978.v
@@ -0,0 +1,27 @@
+Require Import Structures.OrderedType.  
+Require Import Structures.OrderedTypeEx.
+
+Module Type M. Parameter X : Type.      
+
+Declare Module Export XOrd : OrderedType
+  with Definition t := X
+  with Definition eq := @Logic.eq X.
+End M.
+
+Module M' : M.
+  Definition X := nat.
+
+  Module XOrd := Nat_as_OT.
+End M'.
+
+Module Type MyOt.
+  Parameter t : Type.
+  Parameter eq : t -> t -> Prop.
+End MyOt.
+
+Module Type M2. Parameter X : Type.      
+
+Declare Module Export XOrd : MyOt
+  with Definition t := X
+  with Definition eq := @Logic.eq X.
+End M2.
diff --git a/test-suite/bugs/closed/4031.v b/test-suite/bugs/closed/4031.v
new file mode 100644
index 0000000000..2b8641ebb0
--- /dev/null
+++ b/test-suite/bugs/closed/4031.v
@@ -0,0 +1,14 @@
+Definition something (P:Type) (e:P) := e.
+
+Inductive myunit : Set := mytt.
+  (* Proof below works when definition is in Type,
+     however builtin types such as unit are in Set. *)
+
+Lemma demo_hide_generic : 
+   let x := mytt in x = x.
+Proof.
+  intros.
+  change mytt with (@something _ mytt) in x.
+  subst x. (* Proof works if this line is removed *)
+  reflexivity.
+Qed.
\ No newline at end of file