Merge branch 'v8.5'

9 files changed, 353 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v
new file mode 100644
index 0000000000..80695f382c
--- /dev/null
+++ b/test-suite/bugs/closed/3513.v
@@ -0,0 +1,75 @@
+(* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines *)
+Require Coq.Setoids.Setoid.
+Import Coq.Setoids.Setoid.
+Generalizable All Variables.
+Axiom admit : forall {T}, T.
+Class Equiv (A : Type) := equiv : relation A.
+Class type (A : Type) {e : Equiv A} := eq_equiv : Equivalence equiv.
+Class ILogicOps Frm := { lentails: relation Frm;
+                         ltrue: Frm;
+                         land: Frm -> Frm -> Frm;
+                         lor: Frm -> Frm -> Frm }.
+Infix "|--"  := lentails (at level 79, no associativity).
+Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
+Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
+Infix "-|-"  := lequiv (at level 85, no associativity).
+Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
+Section ILogic_Fun.
+  Context (T: Type) `{TType: type T}.
+  Context `{IL: ILogic Frm}.
+  Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit.
+  Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit.
+End ILogic_Fun.
+Implicit Arguments ILFunFrm [[ILOps] [e]].
+Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q;
+                                                   ltrue        := True;
+                                                   land     P Q := P /\ Q;
+                                                   lor      P Q := P \/ Q |}.
+Axiom Action : Set.
+Definition Actions := list Action.
+Instance ActionsEquiv : Equiv Actions := { equiv a1 a2 := a1 = a2 }.
+Definition OPred := ILFunFrm Actions Prop.
+Local Existing Instance ILFun_Ops.
+Local Existing Instance ILFun_ILogic.
+Definition catOP (P Q: OPred) : OPred := admit.
+Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m.
+admit.
+Defined.
+Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit.
+Class IsPointed (T : Type) := point : T.
+Notation IsPointed_OPred P := (IsPointed (exists x : Actions, (P : OPred) x)).
+Record PointedOPred := mkPointedOPred {
+                           OPred_pred :> OPred;
+                           OPred_inhabited: IsPointed_OPred OPred_pred
+                         }.
+Existing Instance OPred_inhabited.
+Canonical Structure default_PointedOPred O `{IsPointed_OPred O} : PointedOPred
+  := {| OPred_pred := O ; OPred_inhabited := _ |}.
+Instance IsPointed_catOP `{IsPointed_OPred P, IsPointed_OPred Q} : IsPointed_OPred (catOP P Q) := admit.
+Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred)
+            (tr : T -> T) (O2 : PointedOPred) (x : T)
+            (H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0),
+     exists e1 e2,
+       catOP (O0 e1) (OPred_pred e2) |-- catOP (O1 x) O2.
+  intros; do 2 esplit.
+  rewrite <- catOPA.
+  lazymatch goal with
+  | |- ?R (?f ?a ?b) (?f ?a' ?b') =>
+    let P := constr:(fun H H' => @Morphisms.proper_prf (OPred -> OPred -> OPred)
+         (@Morphisms.respectful OPred (OPred -> OPred)
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))
+            (@lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop) ==>
+             @lentails OPred
+               (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))) catOP
+         catOP_entails_m_Proper a a' H b b' H') in
+    pose P;
+    refine (P _ _)
+  end; unfold Basics.flip.
+  2: solve [ apply reflexivity ].
+  Undo.
+  2: reflexivity. (* Toplevel input, characters 18-29:
+Error:
+Tactic failure: The relation lentails is not a declared reflexive relation. Maybe you need to require the Setoid library. *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3590.v b/test-suite/bugs/closed/3590.v
new file mode 100644
index 0000000000..51d6744c5c
--- /dev/null
+++ b/test-suite/bugs/closed/3590.v
@@ -0,0 +1,14 @@
+(* Set Primitive Projections. *)
+Set Implicit Arguments.
+Record prod A B := pair { fst : A ; snd : B }.
+Definition idS := Set.
+Goal forall x y : prod Set Set, fst x = fst y.
+  intros.
+  change (@fst _ _ ?z) with (@fst Set idS z) at 2.
+  Unshelve.
+  admit.
+Qed.
+  
+(* Toplevel input, characters 20-58:
+Error: Failed to get enough information from the left-hand side to type the
+right-hand side. *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v
new file mode 100644
index 0000000000..4069e38075
--- /dev/null
+++ b/test-suite/bugs/closed/3690.v
@@ -0,0 +1,52 @@
+Set Printing Universes.
+Set Universe Polymorphism.
+Definition foo (a := Type) (b := Type) (c := Type) := Type.
+Print foo.
+(* foo =
+let a := Type@{Top.1} in
+let b := Type@{Top.2} in let c := Type@{Top.3} in Type@{Top.4}
+     : Type@{Top.4+1}
+(* Top.1
+   Top.2
+   Top.3
+   Top.4 |=  *) *)
+Check @foo. (* foo@{Top.5 Top.6 Top.7
+Top.8}
+     : Type@{Top.8+1}
+(* Top.5
+   Top.6
+   Top.7
+   Top.8 |=  *) *)
+Definition bar := $(let t := eval compute in foo in exact t)$.
+Check @bar. (* bar@{Top.13 Top.14 Top.15
+Top.16}
+     : Type@{Top.16+1}
+(* Top.13
+   Top.14
+   Top.15
+   Top.16 |=  *) *)
+(* The following should fail, since [bar] should only need one universe. *)
+Check @bar@{i j}.
+Definition baz (a := Type) (b := Type : a) (c := Type : b) := a -> c.
+Definition qux := Eval compute in baz.
+Check @qux. (* qux@{Top.24 Top.25
+Top.26}
+     : Type@{max(Top.24+1, Top.26+1)}
+(* Top.24
+   Top.25
+   Top.26 |= Top.25 < Top.24
+              Top.26 < Top.25
+               *) *)
+Print qux. (* qux =
+Type@{Top.21} -> Type@{Top.23}
+     : Type@{max(Top.21+1, Top.23+1)}
+(* Top.21
+   Top.22
+   Top.23 |= Top.22 < Top.21
+              Top.23 < Top.22
+               *) *)
+Fail Check @qux@{Set Set}.
+Fail Check @qux@{Set Set Set}.
+(* [qux] should only need two universes *)
+Check @qux@{i j k}.  (* Error: The command has not failed!, but I think this is suboptimal *)
+Fail Check @qux@{i j}.
diff --git a/test-suite/bugs/closed/3732.v b/test-suite/bugs/closed/3732.v
new file mode 100644
index 0000000000..6e5952a527
--- /dev/null
+++ b/test-suite/bugs/closed/3732.v
@@ -0,0 +1,104 @@
+(* File reduced by coq-bug-finder from original input, then from 2073 lines to 358 lines, then from 359 lines to 218 lines, then from 107 lines to 92 lines *)
+(* coqc version trunk (October 2014) compiled on Oct 11 2014 1:13:41 with OCaml 4.01.0
+   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *)
+Require Coq.Lists.List.
+
+Import Coq.Lists.List.
+
+Set Implicit Arguments.
+Global Set Asymmetric Patterns.
+
+Section machine.
+  Variables pc state : Type.
+
+  Inductive propX (i := pc) (j := state) : list Type -> Type :=
+  | Inj : forall G, Prop -> propX G
+  | ExistsX : forall G A, propX (A :: G) -> propX G.
+
+  Implicit Arguments Inj [G].
+
+  Definition PropX := propX nil.
+  Fixpoint last (G : list Type) : Type.
+    exact (match G with
+             | nil => unit
+             | T :: nil => T
+             | _ :: G' => last G'
+           end).
+  Defined.
+  Fixpoint eatLast (G : list Type) : list Type.
+    exact (match G with
+             | nil => nil
+             | _ :: nil => nil
+             | x :: G' => x :: eatLast G'
+           end).
+  Defined.
+
+  Fixpoint subst G (p : propX G) : (last G -> PropX) -> propX (eatLast G) :=
+    match p with
+      | Inj _ P => fun _ => Inj P
+      | ExistsX G A p1 => fun p' =>
+                            match G return propX (A :: G) -> propX (eatLast (A :: G)) -> propX (eatLast G) with
+                              | nil => fun p1 _ => ExistsX p1
+                              | _ :: _ => fun _ rc => ExistsX rc
+                            end p1 (subst p1 (match G return (last G -> PropX) -> last (A :: G) -> PropX with
+                                                | nil => fun _ _ => Inj True
+                                                | _ => fun p' => p'
+                                              end p'))
+    end.
+
+  Definition spec := state -> PropX.
+  Definition codeSpec := pc -> option spec.
+
+  Inductive valid (specs : codeSpec) (G : list PropX) : PropX -> Prop := Env : forall P, In P G -> valid specs G P.
+  Definition interp specs := valid specs nil.
+End machine.
+Notation "'ExX' : A , P" := (ExistsX (A := A) P) (at level 89) : PropX_scope.
+Bind Scope PropX_scope with PropX propX.
+Variables pc state : Type.
+
+Inductive subs : list Type -> Type :=
+| SNil : subs nil
+| SCons : forall T Ts, (last (T :: Ts) -> PropX pc state) -> subs (eatLast (T :: Ts)) -> subs (T :: Ts).
+
+Fixpoint SPush G T (s : subs G) (f : T -> PropX pc state) : subs (T :: G) :=
+  match s in subs G return subs (T :: G) with
+    | SNil => SCons _ nil f SNil
+    | SCons T' Ts f' s' => SCons T (T' :: Ts) f' (SPush s' f)
+  end.
+
+Fixpoint Substs G (s : subs G) : propX pc state G -> PropX pc state :=
+  match s in subs G return propX pc state G -> PropX pc state with
+    | SNil => fun p => p
+    | SCons _ _ f s' => fun p => Substs s' (subst p f)
+  end.
+Variable specs : codeSpec pc state.
+
+Lemma simplify_fwd_ExistsX : forall G A s (p : propX pc state (A :: G)),
+                               interp specs (Substs s (ExX  : A, p))
+                               -> exists a, interp specs (Substs (SPush s a) p).
+admit.
+Defined.
+
+Goal    forall (G : list Type) (A : Type) (p : propX pc state (@cons Type A G))
+               (s : subs G)
+               (_ : @interp pc state specs (@Substs G s (@ExistsX pc state G A p)))
+               (P : forall _ : subs (@cons Type A G), Prop)
+               (_ : forall (s0 : subs (@cons Type A G))
+                           (_ : @interp pc state specs (@Substs (@cons Type A G) s0 p)),
+                      P s0),
+          @ex (forall _ : A, PropX pc state)
+              (fun a : forall _ : A, PropX pc state => P (@SPush G A s a)).
+  intros ? ? ? ? H ? H'.
+  apply simplify_fwd_ExistsX in H.
+  firstorder. 
+Qed.
+ (* Toplevel input, characters 15-19:
+Error: Illegal application:
+The term "cons" of type "forall A : Type, A -> list A -> list A"
+cannot be applied to the terms
+ "Type" : "Type"
+ "T" : "Type"
+ "G0" : "list Type"
+The 2nd term has type "Type@{Top.53}" which should be coercible to
+ "Type@{Top.12}".
+ *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4046.v b/test-suite/bugs/closed/4046.v
new file mode 100644
index 0000000000..8f8779b7b2
--- /dev/null
+++ b/test-suite/bugs/closed/4046.v
@@ -0,0 +1,6 @@
+Module Import Foo.
+  Class Foo := { foo : Type }.
+End Foo.
+
+Instance f : Foo := { foo := nat }. (* works fine *)
+Instance f' : Foo.Foo := { Foo.foo := nat }. 
diff --git a/test-suite/bugs/closed/4097.v b/test-suite/bugs/closed/4097.v
new file mode 100644
index 0000000000..2109a4cd92
--- /dev/null
+++ b/test-suite/bugs/closed/4097.v
@@ -0,0 +1,64 @@
+(* File reduced by coq-bug-finder from original input, then from 6082 lines to 81 lines, then from 436 lines to 93 lines *)
+(* coqc version 8.5beta1 (February 2015) compiled on Feb 27 2015 15:10:37 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (fc1b3ef9d7270938cd83c524aae0383093b7a4b5) *)
+Global Set Primitive Projections.
+Record sigT {A} (P : A -> Type) := exist { projT1 : A ; projT2 : P projT1 }.
+Arguments projT1 {A P} _ / .
+Arguments projT2 {A P} _ / .
+Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
+Delimit Scope path_scope with path.
+Delimit Scope fibration_scope with fibration.
+Open Scope path_scope.
+Open Scope fibration_scope.
+Notation "( x ; y )" := (exist _ _ x y) : fibration_scope.
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope.
+Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y):
+  p # (f x) = f y
+  :=
+  match p with idpath => idpath end.
+Lemma transport_compose {A B} {x y : A} (P : B -> Type) (f : A -> B)
+  (p : x = y) (z : P (f x))
+  : transport (fun x => P (f x)) p z  =  transport P (ap f p) z.
+admit.
+Defined.
+Generalizable Variables X A B C f g n.
+Definition pr1_path `{P : A -> Type} {u v : sigT P} (p : u = v)
+: u.1 = v.1
+  := ap pr1 p.
+Notation "p ..1" := (pr1_path p) (at level 3) : fibration_scope.
+Definition pr2_path `{P : A -> Type} {u v : sigT P} (p : u = v)
+: p..1 # u.2 = v.2
+  := (transport_compose P pr1 p u.2)^
+     @ (@apD {x:A & P x} _ pr2 _ _ p).
+Notation "p ..2" := (pr2_path p) (at level 3) : fibration_scope.
+Definition path_path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P)
+           (p q : u = v)
+           (rs : {r : p..1 = q..1 & transport (fun x => transport P x u.2 = v.2) r p..2 = q..2})
+: p = q.
+admit.
+Defined.
+Set Debug Unification.
+Definition path_path_sigma {A : Type} (P : A -> Type) (u v : sigT P)
+           (p q : u = v)
+           (r : p..1 = q..1)
+           (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2)
+: p = q
+  := path_path_sigma_uncurried P u v p q (r; s).
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4101.v b/test-suite/bugs/closed/4101.v
new file mode 100644
index 0000000000..a38b050966
--- /dev/null
+++ b/test-suite/bugs/closed/4101.v
@@ -0,0 +1,19 @@
+(* File reduced by coq-bug-finder from original input, then from 10940 lines to 152 lines, then from 509 lines to 163 lines, then from 178 lines to 66 lines *)
+(* coqc version 8.5beta1 (March 2015) compiled on Mar 2 2015 18:53:10 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (e77f178e60918f14eacd1ec0364a491d4cfd0f3f) *)
+
+Global Set Primitive Projections.
+Set Implicit Arguments.
+Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+Axiom path_forall : forall {A : Type} {P : A -> Type} (f g : forall x : A, P x),
+                      (forall x, f x = g x) -> f = g.
+Lemma sigT_obj_eq
+: forall (T : Type) (T0 : T -> Type)
+         (s s0 : forall s : sigT T0,
+                   sigT (fun _ : T0 (projT1 s) => unit) ->
+                   sigT (fun _ : T0 (projT1 s) => unit)),
+   s0 = s.
+Proof.
+  intros.
+  Set Debug Tactic Unification.
+  apply path_forall. 
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4103.v b/test-suite/bugs/closed/4103.v
new file mode 100644
index 0000000000..92cc0279ac
--- /dev/null
+++ b/test-suite/bugs/closed/4103.v
@@ -0,0 +1,12 @@
+Set Primitive Projections.
+
+CoInductive stream A := { hd : A; tl : stream A }.
+
+CoFixpoint ticks (n : nat) : stream unit := {| hd := tt; tl := ticks n |}.
+
+Lemma expand : exists n : nat, (ticks n) = (ticks n).(tl _).
+Proof.
+  eexists.
+  (* Set Debug Tactic Unification. *)
+  (* Set Debug RAKAM. *)
+  reflexivity.
diff --git a/test-suite/bugs/opened/3794.v b/test-suite/bugs/opened/3794.v
new file mode 100644
index 0000000000..99ca6cb39d
--- /dev/null
+++ b/test-suite/bugs/opened/3794.v
@@ -0,0 +1,7 @@
+Hint Extern 10 ((?X = ?Y) -> False) => intros; discriminate.
+Hint Unfold not : core.
+
+Goal true<>false.
+Set Typeclasses Debug.
+Fail typeclasses eauto with core.
+Abort.
\ No newline at end of file