From cd6e8689abff88f03872840d12f177d06fccda05 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 15 May 2015 22:35:51 +0200
Subject: Removing option -no-native-compiler from test #3539 since this option
 is now negated into -native-compiler.

---
 test-suite/bugs/closed/3539.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3539.v b/test-suite/bugs/closed/3539.v
index c862965d4d..d258bb31f8 100644
--- a/test-suite/bugs/closed/3539.v
+++ b/test-suite/bugs/closed/3539.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-no-native-compiler") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 11678 lines to 11330 lines, then from 10721 lines to 9544 lines, then from 9549 lines to 794 lines, then from 810 lines to 785 lines, then from 628 lines to 246 lines, then from 220 lines to 89 lines, then from 80 lines to 47 lines *)
 (* coqc version trunk (August 2014) compiled on Aug 22 2014 4:17:28 with OCaml 4.01.0
    coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (a67cc6941434124465f20b14a1256f2ede31a60e) *)
@@ -63,4 +63,4 @@ x' : forall (_ : T1) (_ : T), T2
 m : T3 (x' fst1 x2) (x' fst0 x2)
 Unable to unify "?25 (@pair ?23 ?24 (fst ?27) (snd ?27))" with
 "?25 ?27".
- *)
\ No newline at end of file
+ *)
-- 
cgit v1.2.3


From 923ce36ed6789718746369847f622b17bb37df2a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 18 May 2015 15:29:55 +0200
Subject: Tentative fix for #3461: Anomaly: Uncaught exception
 Pretype_errors.PretypeError.

Instad of trying to print the exception, we raise it in the tactic monad.
---
 test-suite/bugs/closed/3461.v | 5 +++++
 test-suite/bugs/opened/3461.v | 5 -----
 2 files changed, 5 insertions(+), 5 deletions(-)
 create mode 100644 test-suite/bugs/closed/3461.v
 delete mode 100644 test-suite/bugs/opened/3461.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3461.v b/test-suite/bugs/closed/3461.v
new file mode 100644
index 0000000000..1b625e6a15
--- /dev/null
+++ b/test-suite/bugs/closed/3461.v
@@ -0,0 +1,5 @@
+Lemma foo (b : bool) :
+  exists x : nat, x = x.
+Proof.
+eexists. 
+Fail eexact (eq_refl b).
diff --git a/test-suite/bugs/opened/3461.v b/test-suite/bugs/opened/3461.v
deleted file mode 100644
index 1b625e6a15..0000000000
--- a/test-suite/bugs/opened/3461.v
+++ /dev/null
@@ -1,5 +0,0 @@
-Lemma foo (b : bool) :
-  exists x : nat, x = x.
-Proof.
-eexists. 
-Fail eexact (eq_refl b).
-- 
cgit v1.2.3


From b994685d85d30f0db8ee0ec10f802f6bf3797e4b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 18 May 2015 16:59:50 +0200
Subject: Removing test for opened bugs that were already present in the closed
 test-suite.

---
 test-suite/bugs/opened/3045.v | 30 ------------------------------
 test-suite/bugs/opened/3326.v | 18 ------------------
 test-suite/bugs/opened/3562.v |  2 --
 test-suite/bugs/opened/3657.v | 33 ---------------------------------
 test-suite/bugs/opened/3670.v | 19 -------------------
 test-suite/bugs/opened/3675.v | 20 --------------------
 test-suite/bugs/opened/3788.v |  5 -----
 test-suite/bugs/opened/3808.v |  2 --
 8 files changed, 129 deletions(-)
 delete mode 100644 test-suite/bugs/opened/3045.v
 delete mode 100644 test-suite/bugs/opened/3326.v
 delete mode 100644 test-suite/bugs/opened/3562.v
 delete mode 100644 test-suite/bugs/opened/3657.v
 delete mode 100644 test-suite/bugs/opened/3670.v
 delete mode 100644 test-suite/bugs/opened/3675.v
 delete mode 100644 test-suite/bugs/opened/3788.v
 delete mode 100644 test-suite/bugs/opened/3808.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3


From d5c1f2133a80304ce8a1890e3568b14fafd8f283 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 19 May 2015 18:42:47 +0200
Subject: Test for bug #4116.

---
 test-suite/bugs/closed/4116.v | 383 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 383 insertions(+)
 create mode 100644 test-suite/bugs/closed/4116.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3


From c6714db203f60413523ebeaac86242a6e4cc05e3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 27 May 2015 11:43:10 +0200
Subject: Test for 4159

---
 test-suite/ide/univ.fake | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 test-suite/ide/univ.fake

(limited to 'test-suite')

diff --git a/test-suite/ide/univ.fake b/test-suite/ide/univ.fake
new file mode 100644
index 0000000000..90af8785ad
--- /dev/null
+++ b/test-suite/ide/univ.fake
@@ -0,0 +1,14 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# jumping between broken proofs + interp error while fixing.
+# the error should note make the GUI unfocus the currently focused proof.
+ 
+# first proof
+ADD { Set Implicit Arguments. }
+ADD { Record dynamic := dyn { dyn_type : Type; dyn_value : dyn_type }. }
+ADD { Lemma dyn_inj_type : forall A1 A2 (x1:A1) (x2:A2), dyn x1 = dyn x2 -> A1 = A2. }
+ADD { Proof. }
+ADD { now intros A1 A2 x1 x2 [= e1 e2]. }
+ADD { Qed. }
+JOIN
-- 
cgit v1.2.3


From 5c437ab917bd24de66986e95dcf58c3f31e17a34 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 27 May 2015 11:50:11 +0200
Subject: STM: preserve branch name on edit (Close: #4245, #4246)

---
 test-suite/ide/reopen.fake | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 test-suite/ide/reopen.fake

(limited to 'test-suite')

diff --git a/test-suite/ide/reopen.fake b/test-suite/ide/reopen.fake
new file mode 100644
index 0000000000..8166d0137e
--- /dev/null
+++ b/test-suite/ide/reopen.fake
@@ -0,0 +1,21 @@
+# Script simulating a dialog between coqide and coqtop -ideslave
+# Run it via fake_ide
+#
+# jumping between broken proofs + interp error while fixing.
+# the error should note make the GUI unfocus the currently focused proof.
+ 
+# first proof
+ADD { Lemma a : True. }
+ADD here { Proof using. }
+ADD { fail. }
+ADD { trivial. } # first error
+ADD { Qed. }
+WAIT
+EDIT_AT here
+# Fixing the proof
+ADD fix { trivial. }
+ADD { Qed. }
+WAIT
+EDIT_AT fix
+ADD { Qed. }
+JOIN
-- 
cgit v1.2.3


From e47c30bf431f3c8160b41384eedb538ba16578d0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 29 May 2015 15:41:15 +0200
Subject: Flag -test-mode intended to be used for ad-hoc prints in test-suite

Of course there is an exception to the previous commit.
Fail used to print even if silenced but loading a vernac file.

This behavior is useful only in tests, hence this flag.
---
 test-suite/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index cffbe48196..476d850ac9 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -30,7 +30,7 @@
 BIN := ../bin/
 LIB := ..
 
-coqtop := $(BIN)coqtop -boot -q -batch -R prerequisite TestSuite
+coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite
 bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
 bincoqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
 
-- 
cgit v1.2.3