Merge branch 'v8.5'

7 files changed, 167 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/2946.v b/test-suite/bugs/closed/2946.v
new file mode 100644
index 0000000000..d8138e145c
--- /dev/null
+++ b/test-suite/bugs/closed/2946.v
@@ -0,0 +1,8 @@
+Lemma toto (E : nat -> nat -> Prop) (x y : nat)  
+  (Ex_ : forall z, E x z) (E_y : forall z, E z y) : True.
+
+(* OK *)                                                                     
+assert (pairE1 := let Exy := _ in (Ex_ y, E_y _) : Exy * Exy).               
+
+(* FAIL *)                                                                   
+assert (pairE2 := let Exy := _ in (Ex_ _, E_y x) : Exy * Exy).
diff --git a/test-suite/bugs/closed/3703.v b/test-suite/bugs/closed/3703.v
new file mode 100644
index 0000000000..8f7fe0a09f
--- /dev/null
+++ b/test-suite/bugs/closed/3703.v
@@ -0,0 +1,31 @@
+(* File reduced by coq-bug-finder from original input, then from 6746 lines to 4190 lines, then from 29 lines to 18 lines, then fro\
+m 30 lines to 19 lines *)
+(* coqc version trunk (October 2014) compiled on Oct 7 2014 12:42:41 with OCaml 4.01.0
+   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (2313bde0116a5916912bebbaca77d291f7b2760a) *)
+Record PreCategory := { identity : forall x, x -> x }.
+Definition set_cat : PreCategory := @Build_PreCategory (fun T x => x).
+Module UnKeyed.
+  Global Unset Keyed Unification.
+  Goal forall (T : Type) (g0 g1 : T) (k : T) (H' : forall x : T, k = @identity set_cat T x),
+         ((fun x : T => x) g0) = ((fun x : T => x) g1).
+    intros T g0 g1 k H'.
+    change (identity _ _) with (fun y : T => y) in H';
+      rewrite <- H' || fail "too early".
+    Undo.
+    rewrite <- H'.
+    admit.
+  Defined.
+End UnKeyed.
+Module Keyed.
+  Global Set Keyed Unification.
+  Declare Equivalent Keys (fun x => _) identity.
+  Goal forall (T : Type) (g0 g1 : T) (k : T) (H' : forall x : T, k = @identity set_cat T x),
+         ((fun x : T => x) g0) = ((fun x : T => x) g1).
+    intros T g0 g1 k H'.
+    change (identity _ _) with (fun y : T => y) in H';
+      rewrite <- H' || fail "too early".
+    Undo.
+    rewrite <- H'.
+    admit.
+  Defined.
+End Keyed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v
new file mode 100644
index 0000000000..6b52411752
--- /dev/null
+++ b/test-suite/bugs/closed/3922.v
@@ -0,0 +1,83 @@
+Set Universe Polymorphism.
+Notation Type0 := Set.
+
+Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+
+Notation compose := (fun g f x => g (f x)).
+
+Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.
+Open Scope function_scope.
+
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x)
+  := forall x:A, f x = g x.
+
+Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.
+
+Class Contr_internal (A : Type) := BuildContr {
+  center : A ;
+  contr : (forall y : A, center = y)
+}.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+
+Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope.
+Local Open Scope trunc_scope.
+Notation "-2" := minus_two (at level 0) : trunc_scope.
+Notation "-1" := (-2.+1) (at level 0) : trunc_scope.
+
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | -2 => Contr_internal A
+    | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+
+Class IsTrunc (n : trunc_index) (A : Type) : Type :=
+  Trunc_is_trunc : IsTrunc_internal n A.
+
+Notation Contr := (IsTrunc -2).
+Notation IsHProp := (IsTrunc -1).
+
+Monomorphic Axiom dummy_funext_type : Type0.
+Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }.
+
+Inductive Unit : Type1 :=
+    tt : Unit.
+
+Record TruncType (n : trunc_index) := BuildTruncType {
+  trunctype_type : Type ;
+  istrunc_trunctype_type : IsTrunc n trunctype_type
+}.
+
+Arguments BuildTruncType _ _ {_}.
+
+Coercion trunctype_type : TruncType >-> Sortclass.
+
+Notation "n -Type" := (TruncType n) (at level 1) : type_scope.
+Notation hProp := (-1)-Type.
+
+Notation BuildhProp := (BuildTruncType -1).
+
+Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
+  tr : A -> Trunc n A.
+Arguments tr {n A} a.
+
+Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i})
+: IsTrunc@{j} n (Trunc@{i} n A).
+Admitted.
+
+Definition Trunc_ind {n A}
+  (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)}
+  : (forall a, P (tr a)) -> (forall aa, P aa)
+:= (fun f aa => match aa with tr a => fun _ => f a end Pt).
+Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A).
+Definition cconst_factors_contr `{Funext}  {X Y : Type} (f : X -> Y)
+           (P : Type) `{Pc : X -> Contr P}
+           (g : X -> P) (h : P -> Y) (p : h o g == f)
+: Unit.
+Proof.
+  assert (merely X -> IsHProp P) by admit.
+  refine (let g' := Trunc_ind (fun _ => P) g : merely X -> P in _);
+    [ assumption.. | ].
+  pose (g'' := Trunc_ind (fun _ => P) g : merely X -> P).
diff --git a/test-suite/bugs/closed/3938.v b/test-suite/bugs/closed/3938.v
new file mode 100644
index 0000000000..9844313383
--- /dev/null
+++ b/test-suite/bugs/closed/3938.v
@@ -0,0 +1,7 @@
+Require Import Coq.Arith.PeanoNat.
+Hint Extern 1 => admit : typeclass_instances.
+Require Import Setoid.
+Goal forall a b (f : nat -> Set) (R : nat -> nat -> Prop), 
+       Equivalence R -> R a b -> f a = f b.
+  intros a b f H.
+  intros. Fail rewrite H1. 
diff --git a/test-suite/bugs/closed/3944.v b/test-suite/bugs/closed/3944.v
new file mode 100644
index 0000000000..58e60f4f2e
--- /dev/null
+++ b/test-suite/bugs/closed/3944.v
@@ -0,0 +1,5 @@
+Require Import Setoid.
+Definition C (T : Type) := T.
+Goal forall T (i : C T) (v : T), True.
+Proof.
+Fail setoid_rewrite plus_n_Sm.
diff --git a/test-suite/bugs/closed/3960.v b/test-suite/bugs/closed/3960.v
new file mode 100644
index 0000000000..e56dcef74f
--- /dev/null
+++ b/test-suite/bugs/closed/3960.v
@@ -0,0 +1,26 @@
+Require Program.Tactics.
+
+Axiom foo : nat -> Prop.
+
+Axiom fooP : forall n, foo n.
+
+Class myClass (A: Type) :=
+  {
+    bar : A -> Prop
+  }.
+
+Program Instance myInstance : myClass nat :=
+  {
+    bar := foo
+  }.
+
+Class myClassP (A : Type)  :=
+  {
+    super :> myClass A;
+    barP : forall (a : A), bar a
+  }.
+
+Instance myInstanceP : myClassP nat :=
+  {
+    barP := fooP
+  }.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4035.v b/test-suite/bugs/closed/4035.v
new file mode 100644
index 0000000000..24f340bbd9
--- /dev/null
+++ b/test-suite/bugs/closed/4035.v
@@ -0,0 +1,7 @@
+(* Use of dependent destruction from ltac *)
+Require Import Program.
+Goal nat -> Type.
+  intro x.
+  lazymatch goal with
+  | [ x : nat |- _ ] => dependent destruction x
+  end.