Merge branch 'v8.5'

10 files changed, 383 insertions, 129 deletions

diff --git a/test-suite/bugs/opened/3461.v b/test-suite/bugs/closed/3461.v
index 1b625e6a15..1b625e6a15 100644
--- a/test-suite/bugs/opened/3461.v
+++ b/test-suite/bugs/closed/3461.v
diff --git a/test-suite/bugs/closed/4116.v b/test-suite/bugs/closed/4116.v
new file mode 100644
index 0000000000..f808cb45e9
--- /dev/null
+++ b/test-suite/bugs/closed/4116.v
@@ -0,0 +1,383 @@
+(* File reduced by coq-bug-finder from original input, then from 13191 lines to 1315 lines, then from 1601 lines to 595 lines, then from 585 lines to 379 lines *)
+(* coqc version 8.5beta1 (March 2015) compiled on Mar 3 2015 3:50:31 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ac62cda8a4f488b94033b108c37556877232137a) *)
+
+Axiom admit : False.
+Ltac admit := exfalso; exact admit.
+
+Global Set Primitive Projections.
+
+Notation projT1 := proj1_sig (only parsing).
+Notation projT2 := proj2_sig (only parsing).
+
+Definition relation (A : Type) := A -> A -> Type.
+
+Class Reflexive {A} (R : relation A) :=
+  reflexivity : forall x : A, R x x.
+
+Class Symmetric {A} (R : relation A) :=
+  symmetry : forall x y, R x y -> R y x.
+
+Notation idmap := (fun x => x).
+Delimit Scope function_scope with function.
+Delimit Scope path_scope with path.
+Delimit Scope fibration_scope with fibration.
+Open Scope path_scope.
+Open Scope fibration_scope.
+Open Scope function_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.
+
+Notation compose := (fun g f x => g (f x)).
+
+Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_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.
+
+Global Instance symmetric_paths {A} : Symmetric (@paths A) | 0 := @inverse A.
+
+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 "1" := idpath : path_scope.
+
+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.
+
+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 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.
+
+Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
+: f == g
+  := fun x => match h with idpath => 1 end.
+
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
+  forall x : A, r (s x) = x.
+
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+                                               equiv_inv : B -> A ;
+                                               eisretr : Sect equiv_inv f;
+                                               eissect : Sect f equiv_inv;
+                                               eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
+                                             }.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_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.
+Notation "0" := (-1.+1) : 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.
+
+Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" :=
+  refine (let __transparent_assert_hypothesis := (_ : type) in _);
+  [
+      | (
+        let H := match goal with H := _ |- _ => constr:(H) end in
+        rename H into name) ].
+
+Definition transport_idmap_ap A (P : A -> Type) x y (p : x = y) (u : P x)
+: transport P p u = transport idmap (ap P p) u
+  := match p with idpath => idpath end.
+
+Section Adjointify.
+
+  Context {A B : Type} (f : A -> B) (g : B -> A).
+  Context (isretr : Sect g f) (issect : Sect f g).
+
+  Let issect' := fun x =>
+                   ap g (ap f (issect x)^)  @  ap g (isretr (f x))  @  issect x.
+
+  Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a).
+    admit.
+  Defined.
+
+  Definition isequiv_adjointify : IsEquiv f
+    := BuildIsEquiv A B f g isretr issect' is_adjoint'.
+
+End Adjointify.
+
+Record TruncType (n : trunc_index) := BuildTruncType {
+                                          trunctype_type : Type ;
+                                          istrunc_trunctype_type : IsTrunc n trunctype_type
+                                        }.
+Arguments trunctype_type {_} _.
+
+Coercion trunctype_type : TruncType >-> Sortclass.
+
+Notation "n -Type" := (TruncType n) (at level 1) : type_scope.
+Notation hSet := 0-Type.
+
+Module Export Category.
+  Module Export Core.
+    Set Implicit Arguments.
+
+    Delimit Scope morphism_scope with morphism.
+    Delimit Scope category_scope with category.
+    Delimit Scope object_scope with object.
+
+    Record PreCategory :=
+      Build_PreCategory' {
+          object :> Type;
+          morphism : object -> object -> Type;
+
+          identity : forall x, morphism x x;
+          compose : forall s d d',
+                      morphism d d'
+                      -> morphism s d
+                      -> morphism s d'
+          where "f 'o' g" := (compose f g);
+
+          associativity : forall x1 x2 x3 x4
+                                 (m1 : morphism x1 x2)
+                                 (m2 : morphism x2 x3)
+                                 (m3 : morphism x3 x4),
+                            (m3 o m2) o m1 = m3 o (m2 o m1);
+
+          associativity_sym : forall x1 x2 x3 x4
+                                     (m1 : morphism x1 x2)
+                                     (m2 : morphism x2 x3)
+                                     (m3 : morphism x3 x4),
+                                m3 o (m2 o m1) = (m3 o m2) o m1;
+
+          left_identity : forall a b (f : morphism a b), identity b o f = f;
+          right_identity : forall a b (f : morphism a b), f o identity a = f;
+
+          identity_identity : forall x, identity x o identity x = identity x
+        }.
+    Arguments identity {!C%category} / x%object : rename.
+    Arguments compose {!C%category} / {s d d'}%object (m1 m2)%morphism : rename.
+
+    Definition Build_PreCategory
+               object morphism compose identity
+               associativity left_identity right_identity
+      := @Build_PreCategory'
+           object
+           morphism
+           compose
+           identity
+           associativity
+           (fun _ _ _ _ _ _ _ => symmetry _ _ (associativity _ _ _ _ _ _ _))
+           left_identity
+           right_identity
+           (fun _ => left_identity _ _ _).
+
+    Module Export CategoryCoreNotations.
+      Infix "o" := compose : morphism_scope.
+      Notation "1" := (identity _) : morphism_scope.
+    End CategoryCoreNotations.
+
+  End Core.
+
+End Category.
+Module Export Core.
+  Set Implicit Arguments.
+
+  Delimit Scope functor_scope with functor.
+
+  Local Open Scope morphism_scope.
+
+  Section Functor.
+    Variables C D : PreCategory.
+
+    Record Functor :=
+      {
+        object_of :> C -> D;
+        morphism_of : forall s d, morphism C s d
+                                  -> morphism D (object_of s) (object_of d);
+        composition_of : forall s d d'
+                                (m1 : morphism C s d) (m2: morphism C d d'),
+                           morphism_of _ _ (m2 o m1)
+                           = (morphism_of _ _ m2) o (morphism_of _ _ m1);
+        identity_of : forall x, morphism_of _ _ (identity x)
+                                = identity (object_of x)
+      }.
+  End Functor.
+  Arguments morphism_of [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
+
+End Core.
+Module Export Morphisms.
+  Set Implicit Arguments.
+
+  Local Open Scope category_scope.
+  Local Open Scope morphism_scope.
+
+  Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) :=
+    {
+      morphism_inverse : morphism C d s;
+      left_inverse : morphism_inverse o m = identity _;
+      right_inverse : m o morphism_inverse = identity _
+    }.
+
+  Class Isomorphic {C : PreCategory} s d :=
+    {
+      morphism_isomorphic :> morphism C s d;
+      isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic
+    }.
+
+  Coercion morphism_isomorphic : Isomorphic >-> morphism.
+
+  Local Infix "<~=~>" := Isomorphic (at level 70, no associativity) : category_scope.
+
+  Section iso_equiv_relation.
+    Variable C : PreCategory.
+
+    Global Instance isisomorphism_identity (x : C) : IsIsomorphism (identity x)
+      := {| morphism_inverse := identity x;
+            left_inverse := left_identity C x x (identity x);
+            right_inverse := right_identity C x x (identity x) |}.
+
+    Global Instance isomorphic_refl : Reflexive (@Isomorphic C)
+      := fun x : C => {| morphism_isomorphic := identity x |}.
+
+    Definition idtoiso (x y : C) (H : x = y) : Isomorphic x y
+      := match H in (_ = y0) return (x <~=~> y0) with
+           | 1%path => reflexivity x
+         end.
+  End iso_equiv_relation.
+
+End Morphisms.
+
+Notation IsCategory C := (forall s d : object C, IsEquiv (@idtoiso C s d)).
+
+Notation isotoid C s d := (@equiv_inv _ _ (@idtoiso C s d) _).
+
+Notation cat_of obj :=
+  (@Build_PreCategory obj
+                      (fun x y => x -> y)
+                      (fun _ x => x)
+                      (fun _ _ _ f g => f o g)%core
+                      (fun _ _ _ _ _ _ _ => idpath)
+                      (fun _ _ _ => idpath)
+                      (fun _ _ _ => idpath)
+  ).
+Definition set_cat : PreCategory := cat_of hSet.
+Set Implicit Arguments.
+
+Local Open Scope morphism_scope.
+
+Section Grothendieck.
+  Variable C : PreCategory.
+  Variable F : Functor C set_cat.
+
+  Record Pair :=
+    {
+      c : C;
+      x : F c
+    }.
+
+  Local Notation Gmorphism s d :=
+    { f : morphism C s.(c) d.(c)
+    | morphism_of F f s.(x) = d.(x) }.
+
+  Definition identity_H s
+    := apD10 (identity_of F s.(c)) s.(x).
+
+  Definition Gidentity s : Gmorphism s s.
+  Proof.
+    exists 1.
+    apply identity_H.
+  Defined.
+
+  Definition Gcategory : PreCategory.
+  Proof.
+    refine (@Build_PreCategory
+              Pair
+              (fun s d => Gmorphism s d)
+              Gidentity
+              _
+              _
+              _
+              _); admit.
+  Defined.
+End Grothendieck.
+
+Lemma isotoid_1 {C} `{IsCategory C} {x : C} {H : IsIsomorphism (identity x)}
+: isotoid C x x {| morphism_isomorphic := (identity x) ; isisomorphism_isomorphic := H |}
+  = idpath.
+  admit.
+Defined.
+Generalizable All Variables.
+
+Section Grothendieck2.
+  Context `{IsCategory C}.
+  Variable F : Functor C set_cat.
+
+  Instance iscategory_grothendieck_toset : IsCategory (Gcategory F).
+  Proof.
+    intros s d.
+    refine (isequiv_adjointify _ _ _ _).
+    {
+      intro m.
+      transparent assert (H' : (s.(c) = d.(c))).
+      {
+        apply (idtoiso C (x := s.(c)) (y := d.(c)))^-1%function.
+        exists (m : morphism _ _ _).1.
+        admit.
+
+      }
+      {
+        transitivity {| x := transport (fun x => F x) H' s.(x) |}.
+        admit.
+
+        {
+          change d with {| c := d.(c) ; x := d.(x) |}; simpl.
+          apply ap.
+          subst H'.
+          simpl.
+          refine (transport_idmap_ap _ (fun x => F x : Type) _ _ _ _ @ _ @ (m : morphism _ _ _).2).
+          change (fun x => F x : Type) with (trunctype_type o object_of F)%function.
+          admit.
+        }
+      }
+    }
+    {
+      admit.
+    }
+
+    {
+      intro x.
+      hnf in s, d.
+      destruct x.
+      simpl.
+      erewrite @isotoid_1.
diff --git a/test-suite/bugs/opened/3045.v b/test-suite/bugs/opened/3045.v
deleted file mode 100644
index b7f40b4ad7..0000000000
--- a/test-suite/bugs/opened/3045.v
+++ /dev/null
@@ -1,30 +0,0 @@
-Set Asymmetric Patterns.
-Generalizable All Variables.
-Set Implicit Arguments.
-Set Universe Polymorphism.
-
-Record SpecializedCategory (obj : Type) :=
-  {
-    Object :> _ := obj;
-    Morphism : obj -> obj -> Type;
-
-    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
-  }.
-
-Arguments Compose {obj} [C s d d'] m1 m2 : rename.
-
-Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type :=
-| ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'.
-
-Fixpoint ReifiedMorphismDenote objC C s d (m : @ReifiedMorphism objC C s d) : Morphism C s d :=
-  match m in @ReifiedMorphism objC C s d return Morphism C s d with
-    | ReifiedComposedMorphism _ _ _ _ _ m1 m2 => Compose (@ReifiedMorphismDenote _ _ _ _ m1)
-                                                         (@ReifiedMorphismDenote _ _ _ _ m2)
-  end.
-
-Fixpoint ReifiedMorphismSimplifyWithProof objC C s d (m : @ReifiedMorphism objC C s d)
-: { m' : ReifiedMorphism C s d | ReifiedMorphismDenote m = ReifiedMorphismDenote m' }.
-refine match m with
-         | ReifiedComposedMorphism _ _ s0 d0 d0' m1 m2 => _
-       end; clear m.
-Fail destruct (@ReifiedMorphismSimplifyWithProof _ _ _ _ m1) as [ [] ? ].
diff --git a/test-suite/bugs/opened/3326.v b/test-suite/bugs/opened/3326.v
deleted file mode 100644
index f73117a2ee..0000000000
--- a/test-suite/bugs/opened/3326.v
+++ /dev/null
@@ -1,18 +0,0 @@
-Class ORDER A := Order {
-  LEQ : A -> A -> bool;
-  leqRefl: forall x, true = LEQ x x
-}.
-
-Section XXX.
-
-Variable A:Type.
-Variable (O:ORDER A).
-Definition aLeqRefl := @leqRefl _ O.
-
-Lemma OK : forall x, true = LEQ x x.
-  intros.
-  unfold LEQ.
-  destruct O.
-  clear.
-  Fail apply aLeqRefl. (* Toplevel input, characters 15-30:
-Anomaly: Uncaught exception Not_found(_). Please report. *)
diff --git a/test-suite/bugs/opened/3562.v b/test-suite/bugs/opened/3562.v
deleted file mode 100644
index 04a1223b6e..0000000000
--- a/test-suite/bugs/opened/3562.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Theorem t: True.
-Fail destruct 0 as x.
diff --git a/test-suite/bugs/opened/3657.v b/test-suite/bugs/opened/3657.v
deleted file mode 100644
index 6faec0765e..0000000000
--- a/test-suite/bugs/opened/3657.v
+++ /dev/null
@@ -1,33 +0,0 @@
-(* Set Primitive Projections. *)
-Class foo {A} {a : A} := { bar := a; baz : bar = bar }.
-Arguments bar {_} _ {_}.
-Instance: forall A a, @foo A a.
-intros; constructor.
-abstract reflexivity.
-Defined.
-Goal @bar _ Set _ = (@bar _ (fun _ : Set => Set) _) nat.
-Proof.
-  Check (bar Set).
-  Check (bar (fun _ : Set => Set)).
-  Fail change (bar (fun _ : Set => Set)) with (bar Set). (* Error: Conversion test raised an anomaly *)
-
-Abort.
-
-
-Module A.
-Universes i j.
-Constraint i < j.
-Variable  foo : Type@{i}.
-Goal Type@{i}.
-  Fail let t := constr:(Type@{j}) in
-  change Type with t.
-Abort.
-
-Goal Type@{j}.
-  Fail let t := constr:(Type@{i}) in
-  change Type with t.
-  let t := constr:(Type@{i}) in
-  change t. exact foo.
-Defined.
-
-End A.
diff --git a/test-suite/bugs/opened/3670.v b/test-suite/bugs/opened/3670.v
deleted file mode 100644
index cf5e9b090b..0000000000
--- a/test-suite/bugs/opened/3670.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Module Type FOO.
-  Parameters P Q : Type -> Type.
-End FOO.
-
-Module Type BAR.
-  Declare Module Export foo : FOO.
-  Parameter f : forall A, P A -> Q A -> A.
-End BAR.
-
-Module Type BAZ.
-  Declare Module Export foo : FOO.
-  Parameter g : forall A, P A -> Q A -> A.
-End BAZ.
-
-Module BAR_FROM_BAZ (baz : BAZ) : BAR.
-  Import baz.
-  Module foo <: FOO := foo.
-  Definition f : forall A, P A -> Q A -> A := g.
-End BAR_FROM_BAZ.
diff --git a/test-suite/bugs/opened/3675.v b/test-suite/bugs/opened/3675.v
deleted file mode 100644
index 93227ab852..0000000000
--- a/test-suite/bugs/opened/3675.v
+++ /dev/null
@@ -1,20 +0,0 @@
-Set Primitive Projections.
-Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
-Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
-Arguments idpath {A a} , [A] a.
-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 q) (at level 20) : path_scope.
-Axiom ap : forall {A B:Type} (f:A -> B) {x y:A} (p:x = y), f x = f y.
-Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x.
-Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A ; eisretr : forall x, f (equiv_inv x) = x }.
-Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope.
-Local Open Scope path_scope.
-Local Open Scope equiv_scope.
-Generalizable Variables A B C f g.
-Lemma isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g}
-: IsEquiv (compose g f).
-Proof.
-  refine (Build_IsEquiv A C
-                        (compose g f)
-                        (compose f^-1 g^-1) _).
-  exact (fun c => ap g (@eisretr _ _ f _ (g^-1 c)) @ (@eisretr _ _ g _ c)).
diff --git a/test-suite/bugs/opened/3788.v b/test-suite/bugs/opened/3788.v
deleted file mode 100644
index 8e605a00f6..0000000000
--- a/test-suite/bugs/opened/3788.v
+++ /dev/null
@@ -1,5 +0,0 @@
-Set Implicit Arguments.
-Global Set Primitive Projections.
-Record Functor (C D : Type) := { object_of :> forall _ : C, D }.
-Axiom path_functor_uncurried : forall C D (F G : Functor C D) (_ : sigT (fun HO : object_of F = object_of G => Set)), F = G.
-Fail Lemma path_functor_uncurried_snd C D F G HO HM : (@path_functor_uncurried C D F G (existT _ HO HM)) = HM.
diff --git a/test-suite/bugs/opened/3808.v b/test-suite/bugs/opened/3808.v
deleted file mode 100644
index df40ca1910..0000000000
--- a/test-suite/bugs/opened/3808.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i})
-  := foo : Foo.