Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

20 files changed, 100 insertions, 124 deletions

diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/opened/2456.v
new file mode 100644
index 00000000..6cca5c9f
--- /dev/null
+++ b/test-suite/bugs/opened/2456.v
@@ -0,0 +1,53 @@
+
+Require Import Equality.
+
+Parameter Patch : nat -> nat -> Set.
+
+Inductive Catch (from to : nat) : Type
+    := MkCatch : forall (p : Patch from to),
+                 Catch from to.
+Implicit Arguments MkCatch [from to].
+
+Inductive CatchCommute5
+        : forall {from mid1 mid2 to : nat},
+          Catch from mid1
+       -> Catch mid1 to
+       -> Catch from mid2
+       -> Catch mid2 to
+       -> Prop
+     := MkCatchCommute5 :
+           forall {from mid1 mid2 to : nat}
+                  (p : Patch from mid1)
+                  (q : Patch mid1 to)
+                  (q' : Patch from mid2)
+                  (p' : Patch mid2 to),
+           CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p').
+
+Inductive CatchCommute {from mid1 mid2 to : nat}
+                       (p : Catch from mid1)
+                       (q : Catch mid1 to)
+                       (q' : Catch from mid2)
+                       (p' : Catch mid2 to)
+                     : Prop
+    := isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' p'),
+                         CatchCommute p q q' p'.
+Notation "<< p , q >> <~> << q' , p' >>"
+    := (CatchCommute p q q' p')
+    (at level 60, no associativity).
+
+Lemma CatchCommuteUnique2 :
+      forall {from mid mid' to : nat}
+             {p   : Catch from mid}  {q   : Catch mid  to}
+             {q'  : Catch from mid'} {p'  : Catch mid' to}
+             {q'' : Catch from mid'} {p'' : Catch mid' to}
+             (commute1 : <<p, q>> <~> <<q', p'>>)
+             (commute2 : <<p, q>> <~> <<q'', p''>>),
+      (p' = p'') /\ (q' = q'').
+Proof with auto.
+intros.
+set (X := commute2).
+Fail dependent destruction commute1;
+dependent destruction catchCommuteDetails;
+dependent destruction commute2;
+dependent destruction catchCommuteDetails generalizing X.
+Admitted.
diff --git a/test-suite/bugs/opened/2951.v b/test-suite/bugs/opened/2951.v
deleted file mode 100644
index 3739247b..00000000
--- a/test-suite/bugs/opened/2951.v
+++ /dev/null
@@ -1 +0,0 @@
-Class C (A: Type) : Type := { f: A }.
diff --git a/test-suite/bugs/opened/3071.v b/test-suite/bugs/opened/3071.v
deleted file mode 100644
index 611ac606..00000000
--- a/test-suite/bugs/opened/3071.v
+++ /dev/null
@@ -1,5 +0,0 @@
-Definition foo := True.
-
-Section foo.
-  Global Arguments foo / .
-Fail End foo.
diff --git a/test-suite/bugs/opened/3263.v b/test-suite/bugs/opened/3263.v
index 6de13f74..f0c707bd 100644
--- a/test-suite/bugs/opened/3263.v
+++ b/test-suite/bugs/opened/3263.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines,  2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *)
 Generalizable All Variables.
 Set Implicit Arguments.
diff --git a/test-suite/bugs/opened/3298.v b/test-suite/bugs/opened/3298.v
deleted file mode 100644
index bce7c3f2..00000000
--- a/test-suite/bugs/opened/3298.v
+++ /dev/null
@@ -1,23 +0,0 @@
-Module JGross.
-  Hint Extern 1 => match goal with |- match ?E with end => case E end.
-
-  Goal forall H : False, match H return Set with end.
-  Proof.
-    intros.
-    Fail solve [ eauto ]. (* No applicable tactic *)
-    admit.
-  Qed.
-End JGross.
-
-Section BenDelaware.
-  Hint Extern 0 => admit.
-  Goal forall (H : False), id (match H return Set with end).
-  Proof.
-    eauto.
-  Qed.
-  Goal forall (H : False), match H return Set with end.
-  Proof.
-    Fail solve [ eauto ] .
-    admit.
-  Qed.
-End BenDelaware.
diff --git a/test-suite/bugs/opened/3345.v b/test-suite/bugs/opened/3345.v
index b61174a8..3e3da6df 100644
--- a/test-suite/bugs/opened/3345.v
+++ b/test-suite/bugs/opened/3345.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 1972 lines to 136 lines, then from 119 lines to 105 lines *)
 Global Set Implicit Arguments.
 Require Import Coq.Lists.List Program.
diff --git a/test-suite/bugs/opened/3395.v b/test-suite/bugs/opened/3395.v
index ff0dbf97..5ca48fc9 100644
--- a/test-suite/bugs/opened/3395.v
+++ b/test-suite/bugs/opened/3395.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines,  2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *)
 Generalizable All Variables.
 Set Implicit Arguments.
diff --git a/test-suite/bugs/opened/3467.v b/test-suite/bugs/opened/3467.v
deleted file mode 100644
index 900bfc34..00000000
--- a/test-suite/bugs/opened/3467.v
+++ /dev/null
@@ -1,6 +0,0 @@
-Module foo.
-  Notation x := $(exact I)$.
-End foo.
-Module bar.
-  Fail Include foo.
-End bar.
diff --git a/test-suite/bugs/opened/3490.v b/test-suite/bugs/opened/3490.v
deleted file mode 100644
index e7a5caa1..00000000
--- a/test-suite/bugs/opened/3490.v
+++ /dev/null
@@ -1,27 +0,0 @@
-Inductive T : Type :=                                                                                        
-| Var : nat -> T                                                                                                 
-| Arr : T -> T -> T.                                                                                             
-
-Inductive Tele : list T -> Type :=                                                                               
-| Tnil  : @Tele nil                                                                                              
-| Tcons : forall ls, forall (t : @Tele ls) (l : T), @Tele (l :: ls). 
-
-Fail Fixpoint TeleD (ls : list T) (t : Tele ls) {struct t}
-   : { x : Type & x -> nat -> Type } :=
-     match t return { x : Type & x -> nat -> Type } with
-       | Tnil => @existT Type (fun x => x -> nat -> Type) unit (fun (_ : unit) (_ : nat) => unit)
-       | Tcons ls t' l =>
-         let (result, get) := TeleD ls t' in
-         @existT Type (fun x => x -> nat -> Type)
-                 { v : result & (fix TD (t : T) {struct t} :=
-                                   match  t with
-                                     | Var n =>
-                                       get v n
-                                     | Arr a b => TD a -> TD b
-                                   end) l }
-                 (fun x n =>
-                    match n return Type with
-                      | 0 => projT2 x
-                      | S n => get (projT1 x) n
-                    end)
-     end.
diff --git a/test-suite/bugs/opened/3491.v b/test-suite/bugs/opened/3491.v
deleted file mode 100644
index 9837b0ec..00000000
--- a/test-suite/bugs/opened/3491.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Fail Inductive list (A : Type) (T := A) : Type :=
-    nil : list A | cons : T -> list T -> list A.
diff --git a/test-suite/bugs/opened/3509.v b/test-suite/bugs/opened/3509.v
index 02e47a8b..3913bbb4 100644
--- a/test-suite/bugs/opened/3509.v
+++ b/test-suite/bugs/opened/3509.v
@@ -1,3 +1,4 @@
+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
diff --git a/test-suite/bugs/opened/3510.v b/test-suite/bugs/opened/3510.v
index 25285636..daf26507 100644
--- a/test-suite/bugs/opened/3510.v
+++ b/test-suite/bugs/opened/3510.v
@@ -1,3 +1,4 @@
+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
diff --git a/test-suite/bugs/opened/3593.v b/test-suite/bugs/opened/3593.v
new file mode 100644
index 00000000..d83b9006
--- /dev/null
+++ b/test-suite/bugs/opened/3593.v
@@ -0,0 +1,10 @@
+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/3681.v b/test-suite/bugs/opened/3681.v
deleted file mode 100644
index 194113c6..00000000
--- a/test-suite/bugs/opened/3681.v
+++ /dev/null
@@ -1,20 +0,0 @@
-Module Type FOO.
-  Parameters P Q : Type -> Type.
-End FOO.
-
-Module Type BAR.
-  Declare Module Import 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.
-  Import foo.
-  Definition f : forall A, P A -> Q A -> A := g.
-End BAR_FROM_BAZ.
diff --git a/test-suite/bugs/opened/3685.v b/test-suite/bugs/opened/3685.v
index d647b5a8..b2b5db6b 100644
--- a/test-suite/bugs/opened/3685.v
+++ b/test-suite/bugs/opened/3685.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
 Set Universe Polymorphism.
 Class Funext := { }.
 Delimit Scope category_scope with category.
diff --git a/test-suite/bugs/opened/3754.v b/test-suite/bugs/opened/3754.v
index c7441882..9b3f94d9 100644
--- a/test-suite/bugs/opened/3754.v
+++ b/test-suite/bugs/opened/3754.v
@@ -1,3 +1,4 @@
+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
    coqtop version trunk (October 2014) *)
diff --git a/test-suite/bugs/opened/3786.v b/test-suite/bugs/opened/3786.v
deleted file mode 100644
index 5a124115..00000000
--- a/test-suite/bugs/opened/3786.v
+++ /dev/null
@@ -1,40 +0,0 @@
-Require Coq.Lists.List.
-Require Coq.Sets.Ensembles.
-Import Coq.Sets.Ensembles.
-Global Set Implicit Arguments.
-Delimit Scope comp_scope with comp.
-Inductive Comp : Type -> Type :=
-| Return : forall A, A -> Comp A
-| Bind : forall A B, Comp A -> (A -> Comp B) -> Comp B
-| Pick : forall A, Ensemble A -> Comp A.
-Notation ret := Return.
-Notation "x <- y ; z" := (Bind y%comp (fun x => z%comp))
-                           (at level 81, right associativity,
-                            format "'[v' x  <-  y ; '/' z ']'") : comp_scope.
-Axiom refine : forall {A} (old : Comp A) (new : Comp A), Prop.
-Open Scope comp.
-Axiom elements : forall {A} (ls : list A), Ensemble A.
-Axiom to_list : forall {A} (S : Ensemble A), Comp (list A).
-Axiom finite_set_handle_cardinal : refine (ret 0) (ret 0).
-Definition sumUniqueSpec (ls : list nat) : Comp nat.
-  exact (ls' <- to_list (elements ls);
-         List.fold_right (fun a b' => Bind b' ((fun a b => ret (a + b)) a)) (ret 0) ls').
-Defined.
-Axiom admit : forall {T}, T.
-Definition sumUniqueImpl (ls : list nat)
-: { c : _ | refine (sumUniqueSpec ls) (ret c) }%type.
-Proof.
-  eexists.
-  match goal with
-    | [ |- refine ?a ?b ] => let a' := eval hnf in a in refine (_ : refine a' b)
-  end;
-  try setoid_rewrite (@finite_set_handle_cardinal).
-  Undo.
-  match goal with
-    | [ |- refine ?a ?b ] => let a' := eval hnf in a in change (refine a' b)
-  end.
-  try setoid_rewrite (@finite_set_handle_cardinal). (* Anomaly: Uncaught exception Invalid_argument("decomp_pointwise").
-Please report. *)
-  instantiate (1 := admit).
-  admit.
-Defined.
diff --git a/test-suite/bugs/opened/3794.v b/test-suite/bugs/opened/3794.v
new file mode 100644
index 00000000..99ca6cb3
--- /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
diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/opened/3848.v
new file mode 100644
index 00000000..a03e8ffd
--- /dev/null
+++ b/test-suite/bugs/opened/3848.v
@@ -0,0 +1,22 @@
+Require Import TestSuite.admit.
+Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x.
+Class IsEquiv {A B} (f : A -> B) := { equiv_inv : B -> A ; eisretr : Sect equiv_inv f }.
+Arguments eisretr {A B} f {_} _.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'").
+Generalizable Variables A B f g e n.
+Definition functor_forall `{P : A -> Type} `{Q : B -> Type}
+           (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b)
+: (forall a:A, P a) -> (forall b:B, Q b).
+  admit.
+Defined.
+
+Lemma isequiv_functor_forall `{P : A -> Type} `{Q : B -> Type}
+      `{IsEquiv B A f} `{forall b, @IsEquiv (P (f b)) (Q b) (g b)}
+: (forall b : B, Q b) -> forall a : A, P a.
+Proof.
+  refine (functor_forall
+            (f^-1)
+            (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)).
+Fail Defined. (* Error: Attempt to save an incomplete proof *)
diff --git a/test-suite/bugs/opened/HoTT_coq_120.v b/test-suite/bugs/opened/HoTT_coq_120.v
index 7847c5e4..05ee6c7b 100644
--- a/test-suite/bugs/opened/HoTT_coq_120.v
+++ b/test-suite/bugs/opened/HoTT_coq_120.v
@@ -1,3 +1,4 @@
+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.