Imported Upstream version 8.5~beta3+dfsg

17 files changed, 6 insertions, 421 deletions

diff --git a/test-suite/bugs/opened/3045.v b/test-suite/bugs/opened/3045.v
deleted file mode 100644
index b7f40b4a..00000000
--- 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 f73117a2..00000000
--- 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/3461.v b/test-suite/bugs/opened/3461.v
deleted file mode 100644
index 1b625e6a..00000000
--- 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).
diff --git a/test-suite/bugs/opened/3509.v b/test-suite/bugs/opened/3509.v
deleted file mode 100644
index 3913bbb4..00000000
--- a/test-suite/bugs/opened/3509.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Require Import TestSuite.admit.
-Lemma match_bool_fn b A B xT xF
-: match b as b return forall x : A, B b x with
-    | true => xT
-    | false => xF
-  end
-  = fun x : A => match b as b return B b x with
-                   | true => xT x
-                   | false => xF x
-                 end.
-admit.
-Defined.
-Lemma match_bool_comm_1 (b : bool) A B (F : forall x : A, B x) t f
-: (if b as b return B (if b then t else f) then F t else F f)
-  = F (if b then t else f).
-admit.
-Defined.
-Hint Rewrite match_bool_fn : matchdb.
-Fail Hint Rewrite match_bool_comm_1 : matchdb.
diff --git a/test-suite/bugs/opened/3510.v b/test-suite/bugs/opened/3510.v
deleted file mode 100644
index daf26507..00000000
--- a/test-suite/bugs/opened/3510.v
+++ /dev/null
@@ -1,35 +0,0 @@
-Require Import TestSuite.admit.
-Lemma match_option_fn T (b : option T) A B s n
-: match b as b return forall x : A, B b x with
-    | Some k => s k
-    | None => n
-  end
-  = fun x : A => match b as b return B b x with
-                   | Some k => s k x
-                   | None => n x
-                 end.
-admit.
-Defined.
-Lemma match_option_comm_2 T (p : option T) A B R (f : forall (x : A) (y : B x), R x y) (s1 : T -> A) (s2 : forall x : T, B (s1 x)) n1 n2
-: match p as p return R match p with
-                          | Some k => s1 k
-                          | None => n1
-                        end
-                        match p as p return B match p with Some k => s1 k | None => n1 end with
-                          | Some k => s2 k
-                          | None => n2
-                        end with
-    | Some k => f (s1 k) (s2 k)
-    | None => f n1 n2
-  end
-  = f match p return A with
-        | Some k => s1 k
-        | None => n1
-      end
-      match p as p return B match p with Some k => s1 k | None => n1 end with
-        | Some k => s2 k
-        | None => n2
-      end.
-admit.
-Defined.
-Fail Hint Rewrite match_option_fn match_option_comm_2 : matchdb.
diff --git a/test-suite/bugs/opened/3562.v b/test-suite/bugs/opened/3562.v
deleted file mode 100644
index 04a1223b..00000000
--- 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/3593.v b/test-suite/bugs/opened/3593.v
deleted file mode 100644
index d83b9006..00000000
--- a/test-suite/bugs/opened/3593.v
+++ /dev/null
@@ -1,10 +0,0 @@
-Set Universe Polymorphism.
-Set Printing All.
-Set Implicit Arguments.
-Record prod A B := pair { fst : A ; snd : B }.
-Goal forall x : prod Set Set, let f := @fst _ in f _ x = @fst _ _ x.
-simpl; intros.
-  constr_eq (@fst Set Set x) (fst (A := Set) (B := Set) x).   
-  Fail Fail progress change (@fst Set Set x) with (fst (A := Set) (B := Set) x).
-  reflexivity.
-Qed.
diff --git a/test-suite/bugs/opened/3657.v b/test-suite/bugs/opened/3657.v
deleted file mode 100644
index 6faec076..00000000
--- 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 cf5e9b09..00000000
--- 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 93227ab8..00000000
--- 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/3685.v b/test-suite/bugs/opened/3685.v
deleted file mode 100644
index b2b5db6b..00000000
--- a/test-suite/bugs/opened/3685.v
+++ /dev/null
@@ -1,75 +0,0 @@
-Require Import TestSuite.admit.
-Set Universe Polymorphism.
-Class Funext := { }.
-Delimit Scope category_scope with category.
-Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
-Set Implicit Arguments.
-Record Functor (C D : PreCategory) :=
-  { object_of :> C -> D;
-    morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d);
-    identity_of : forall s m, morphism_of s s m = morphism_of s s m }.
-Definition sub_pre_cat `{Funext} (P : PreCategory -> Type) : PreCategory.
-Proof.
-  exact (@Build_PreCategory PreCategory Functor).
-Defined.
-Definition opposite (C : PreCategory) : PreCategory.
-Proof.
-  exact (@Build_PreCategory C (fun s d => morphism C d s)).
-Defined.
-Local Notation "C ^op" := (opposite C) (at level 3, format "C '^op'") : category_scope.
-Definition prod (C D : PreCategory) : PreCategory.
-Proof.
-  refine (@Build_PreCategory
-            (C * D)%type
-            (fun s d => (morphism C (fst s) (fst d) * morphism D (snd s) (snd d))%type)).
-Defined.
-Local Infix "*" := prod : category_scope.
-Record NaturalTransformation C D (F G : Functor C D) := {}.
-Definition functor_category (C D : PreCategory) : PreCategory.
-Proof.
-  exact (@Build_PreCategory (Functor C D) (@NaturalTransformation C D)).
-Defined.
-Local Notation "C -> D" := (functor_category C D) : category_scope.
-Module Export PointwiseCore.
-  Local Open Scope category_scope.
-  Definition pointwise
-             (C C' : PreCategory)
-             (F : Functor C' C)
-             (D D' : PreCategory)
-             (G : Functor D D')
-  : Functor (C -> D) (C' -> D').
-  Proof.
-    refine (Build_Functor
-              (C -> D) (C' -> D')
-              _
-              _
-              _);
-    abstract admit.
-  Defined.
-End PointwiseCore.
-Axiom Pidentity_of : forall (C D : PreCategory) (F : Functor C C) (G : Functor D D), pointwise F G = pointwise F G.
-Local Open Scope category_scope.
-Module Success.
-  Definition functor_uncurried `{Funext} (P : PreCategory -> Type)
-             (has_functor_categories : forall C D : sub_pre_cat P, P (C -> D))
-  : object (((sub_pre_cat P)^op * (sub_pre_cat P)) -> (sub_pre_cat P))
-    := Eval cbv zeta in
-        let object_of := (fun CD => (((fst CD) -> (snd CD))))
-        in Build_Functor
-             ((sub_pre_cat P)^op * (sub_pre_cat P)) (sub_pre_cat P)
-             object_of
-             (fun CD C'D' FG => pointwise (fst FG) (snd FG))
-             (fun _ _ => @Pidentity_of _ _ _ _).
-End Success.
-Module Bad.
-  Include PointwiseCore.
-  Fail Definition functor_uncurried `{Funext} (P : PreCategory -> Type)
-             (has_functor_categories : forall C D : sub_pre_cat P, P (C -> D))
-  : object (((sub_pre_cat P)^op * (sub_pre_cat P)) -> (sub_pre_cat P))
-    := Eval cbv zeta in
-        let object_of := (fun CD => (((fst CD) -> (snd CD))))
-        in Build_Functor
-             ((sub_pre_cat P)^op * (sub_pre_cat P)) (sub_pre_cat P)
-             object_of
-             (fun CD C'D' FG => pointwise (fst FG) (snd FG))
-             (fun _ _ => @Pidentity_of _ _ _ _).
diff --git a/test-suite/bugs/opened/3754.v b/test-suite/bugs/opened/3754.v
index 9b3f94d9..a717bbe7 100644
--- a/test-suite/bugs/opened/3754.v
+++ b/test-suite/bugs/opened/3754.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *)
 (* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1
diff --git a/test-suite/bugs/opened/3788.v b/test-suite/bugs/opened/3788.v
deleted file mode 100644
index 8e605a00..00000000
--- 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 df40ca19..00000000
--- 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.
diff --git a/test-suite/bugs/opened/3819.v b/test-suite/bugs/opened/3819.v
deleted file mode 100644
index 7105a658..00000000
--- a/test-suite/bugs/opened/3819.v
+++ /dev/null
@@ -1,11 +0,0 @@
-Set Universe Polymorphism.
-
-Record Op := { t : Type ; op : t -> t }.
-
-Canonical Structure OpType : Op := Build_Op Type (fun X => X).
-
-Lemma test1 (X:Type) : eq (op OpType X)  X.
-Proof eq_refl.
-
-Lemma test2 (A:Type) : eq (op _ A)  A.
-Fail Proof eq_refl.
diff --git a/test-suite/bugs/opened/4214.v b/test-suite/bugs/opened/4214.v
new file mode 100644
index 00000000..3daf4521
--- /dev/null
+++ b/test-suite/bugs/opened/4214.v
@@ -0,0 +1,5 @@
+(* Check that subst uses all equations around *)
+Goal forall A (a b c : A), b = a -> b = c -> a = c.
+intros.
+subst.
+Fail reflexivity.
diff --git a/test-suite/bugs/opened/HoTT_coq_120.v b/test-suite/bugs/opened/HoTT_coq_120.v
deleted file mode 100644
index 05ee6c7b..00000000
--- a/test-suite/bugs/opened/HoTT_coq_120.v
+++ /dev/null
@@ -1,137 +0,0 @@
-Require Import TestSuite.admit.
-(* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from 351 lines to 260 lines, then from 208 lines to 162 lines, then from 167 lines to 154 lines *)
-Set Universe Polymorphism.
-Generalizable All Variables.
-Reserved Notation "g 'o' f" (at level 40, left associativity).
-Inductive paths {A : Type} (a : A) : A -> Type :=
-  idpath : paths a a.
-Arguments idpath {A a} , [A] a.
-Notation "x = y" := (@paths _ x y) : type_scope.
-
-Class IsEquiv {A B : Type} (f : A -> B) := {}.
-
-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.
-
-Fixpoint nat_to_trunc_index (n : nat) : trunc_index
-  := match n with
-       | 0 => trunc_S (trunc_S minus_two)
-       | S n' => trunc_S (nat_to_trunc_index n')
-     end.
-
-Coercion nat_to_trunc_index : nat >-> trunc_index.
-
-Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
-  match n with
-    | minus_two => Contr_internal A
-    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
-  end.
-
-Notation minus_one:=(trunc_S minus_two).
-
-Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A.
-
-Notation Contr := (IsTrunc minus_two).
-Notation IsHProp := (IsTrunc minus_one).
-Notation IsHSet := (IsTrunc 0).
-
-Class Funext := {}.
-Inductive Unit : Set := tt.
-
-Instance contr_unit : Contr Unit | 0 := let x := {|
-                                              center := tt;
-                                              contr := fun t : Unit => match t with tt => idpath end
-                                            |} in x.
-Instance trunc_succ `{IsTrunc n A} : IsTrunc (trunc_S n) A | 1000.
-admit.
-Defined.
-Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}.
-Definition Unit_hp:hProp:=(hp Unit _).
-Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
-Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
-Definition ismono {X Y} (f : X -> Y)
-  := forall Z : hSet,
-     forall g h : Z -> X, (fun x => f (g x)) = (fun x => f (h x)) -> g = h.
-
-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;
-      compose : forall s d d', morphism d d' -> morphism s d -> morphism s d'
-    }.
-Arguments compose [!C s d d'] m1 m2 : rename.
-
-Infix "o" := compose : morphism_scope.
-Local Open Scope morphism_scope.
-
-Class IsEpimorphism {C} {x y} (m : morphism C x y) :=
-  is_epimorphism : forall z (m1 m2 : morphism C y z),
-                     m1 o m = m2 o m
-                     -> m1 = m2.
-
-Class IsMonomorphism {C} {x y} (m : morphism C x y) :=
-  is_monomorphism : forall z (m1 m2 : morphism C z x),
-                      m o m1 = m o m2
-                      -> m1 = m2.
-Class Univalence := {}.
-Global Instance isset_hProp `{Funext} : IsHSet hProp | 0. Admitted.
-
-Definition set_cat : PreCategory
-  := @Build_PreCategory hSet
-                        (fun x y => forall _ : x, y)%core
-                        (fun _ _ _ f g x => f (g x))%core.
-Local Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A.
-Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. Admitted.
-Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT  P).
-Definition isepi {X Y} `(f:X->Y) := forall Z: hSet,
-                                    forall g h: Y -> Z, (fun x => g (f x)) = (fun x => h (f x)) -> g = h.
-Definition issurj {X Y} (f:X->Y) := forall y:Y , hexists (fun x => (f x) = y).
-Lemma isepi_issurj `{fs:Funext} `{ua:Univalence} `{fs' : Funext} {X Y} (f:X->Y): isepi f -> issurj f.
-Proof.
-  intros epif y.
-  set (g :=fun _:Y => Unit_hp).
-  set (h:=(fun y:Y => (hp (hexists (fun _ : Unit => {x:X & y = (f x)})) _ ))).
-  clear fs'.
-  hnf in epif.
-  specialize (epif (BuildhSet hProp _) g h).
-  admit.
-Defined.
-Definition isequiv_isepi_ismono `{Univalence, fs0 : Funext} (X Y : hSet) (f : X -> Y) (epif : isepi f) (monof : ismono f)
-: IsEquiv f.
-Proof.
-  pose proof (@isepi_issurj _ _ _ _ _ f epif) as surjf.
-  admit.
-Defined.
-Section fully_faithful_helpers.
-  Context `{fs0 : Funext}.
-  Variables x y : hSet.
-  Variable m : x -> y.
-
-  Let isequiv_isepi_ismono_helper ua := (@isequiv_isepi_ismono ua fs0 x y m : isepi m -> ismono m -> IsEquiv m).
-
-  Goal True.
-  Fail set (isequiv_isepimorphism_ismonomorphism
-       := fun `{Univalence}
-              (Hepi : IsEpimorphism (m : morphism set_cat x y))
-              (Hmono : IsMonomorphism (m : morphism set_cat x y))
-          => (@isequiv_isepi_ismono_helper _ Hepi Hmono : @IsEquiv _ _ m)).
-  admit.
-  Undo.
-  Fail set (isequiv_isepimorphism_ismonomorphism'
-       := fun `{Univalence}
-              (Hepi : IsEpimorphism (m : morphism set_cat x y))
-              (Hmono : IsMonomorphism (m : morphism set_cat x y))
-          => ((let _ := @isequiv_isepimorphism_ismonomorphism _ Hepi Hmono in @isequiv_isepi_ismono _ fs0 x y m Hepi Hmono)
-              : @IsEquiv _ _ m)).
-  Set Printing Universes.
-  admit. (* Error: Universe inconsistency (cannot enforce Top.235 <= Set because Set
-< Top.235). *)