From 061519fe518fc090a727957f7e46cbe67e10c633 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 24 Feb 2015 11:39:34 +0100
Subject: Univs: Fix Check calling the kernel to retype in the wrong
 environment. Fixes bug #4089.

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

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v
new file mode 100644
index 0000000000..0ccbf5652f
--- /dev/null
+++ b/test-suite/bugs/closed/4089.v
@@ -0,0 +1,373 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *)
+(* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *)
+Open Scope type_scope.
+
+Global Set Universe Polymorphism.
+Module Export Datatypes.
+
+Set Implicit Arguments.
+
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+End Datatypes.
+Module Export Specif.
+
+Set Implicit Arguments.
+
+Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P proj1_sig }.
+
+Notation sigT := sig (only parsing).
+Notation existT := exist (only parsing).
+
+Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
+
+Notation projT1 := proj1_sig (only parsing).
+Notation projT2 := proj2_sig (only parsing).
+
+End Specif.
+
+Ltac rapply p :=
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _ _) ||
+  refine (p _ _ _ _ _) ||
+  refine (p _ _ _ _) ||
+  refine (p _ _ _) ||
+  refine (p _ _) ||
+  refine (p _) ||
+  refine p.
+
+Local Unset Elimination Schemes.
+
+Definition relation (A : Type) := A -> A -> Type.
+
+Class Symmetric {A} (R : relation A) :=
+  symmetry : forall x y, R x y -> R y x.
+
+Class Transitive {A} (R : relation A) :=
+  transitivity : forall x y z, R x y -> R y z -> R x z.
+
+Tactic Notation "etransitivity" open_constr(y) :=
+  let R := match goal with |- ?R ?x ?z => constr:(R) end in
+  let x := match goal with |- ?R ?x ?z => constr:(x) end in
+  let z := match goal with |- ?R ?x ?z => constr:(z) end in
+  let pre_proof_term_head := constr:(@transitivity _ R _) in
+  let proof_term_head := (eval cbn in pre_proof_term_head) in
+  refine (proof_term_head x y z _ _); [ change (R x y) | change (R y z) ].
+
+Ltac transitivity x := etransitivity x.
+
+Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+
+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 fibration_scope.
+Open Scope function_scope.
+
+Notation "( x ; y )" := (existT _ 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.
+
+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.
+
+Scheme paths_ind := Induction for paths Sort Type.
+
+Definition paths_rect := paths_ind.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Local Open Scope path_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.
+
+Arguments concat {A x y z} p q : simpl nomatch.
+
+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)
+}.
+
+Arguments eisretr {A B}%type_scope f%function_scope {_} _.
+Arguments eissect {A B}%type_scope f%function_scope {_} _.
+Arguments eisadj {A B}%type_scope f%function_scope {_} _.
+
+Record Equiv A B := BuildEquiv {
+  equiv_fun : A -> B ;
+  equiv_isequiv : IsEquiv equiv_fun
+}.
+
+Coercion equiv_fun : Equiv >-> Funclass.
+
+Global Existing Instance equiv_isequiv.
+
+Bind Scope equiv_scope with Equiv.
+
+Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope.
+
+Inductive Unit : Type1 :=
+    tt : Unit.
+
+Ltac done :=
+  trivial; intros; solve
+    [ repeat first
+      [ solve [trivial]
+      | solve [symmetry; trivial]
+      | reflexivity
+
+      | contradiction
+      | split ]
+    | match goal with
+      H : ~ _ |- _ => solve [destruct H; trivial]
+      end ].
+Tactic Notation "by" tactic(tac) :=
+  tac; done.
+
+Definition concat_p1 {A : Type} {x y : A} (p : x = y) :
+  p @ 1 = p
+  :=
+  match p with idpath => 1 end.
+
+Definition concat_1p {A : Type} {x y : A} (p : x = y) :
+  1 @ p = p
+  :=
+  match p with idpath => 1 end.
+
+Definition ap_pp {A B : Type} (f : A -> B) {x y z : A} (p : x = y) (q : y = z) :
+  ap f (p @ q) = (ap f p) @ (ap f q)
+  :=
+  match q with
+    idpath =>
+    match p with idpath => 1 end
+  end.
+
+Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) :
+  ap (g o f) p = ap g (ap f p)
+  :=
+  match p with idpath => 1 end.
+
+Definition concat_A1p {A : Type} {f : A -> A} (p : forall x, f x = x) {x y : A} (q : x = y) :
+  (ap f q) @ (p y) = (p x) @ q
+  :=
+  match q with
+    | idpath => concat_1p _ @ ((concat_p1 _) ^)
+  end.
+
+Definition concat2 {A} {x y z : A} {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q')
+  : p @ q = p' @ q'
+:= match h, h' with idpath, idpath => 1 end.
+
+Notation "p @@ q" := (concat2 p q)%path (at level 20) : path_scope.
+
+Definition whiskerL {A : Type} {x y z : A} (p : x = y)
+  {q r : y = z} (h : q = r) : p @ q = p @ r
+:= 1 @@ h.
+
+Definition ap02 {A B : Type} (f:A->B) {x y:A} {p q:x=y} (r:p=q) : ap f p = ap f q
+  := match r with idpath => 1 end.
+Module Export Equivalences.
+
+Generalizable Variables A B C f g.
+
+Global Instance isequiv_idmap (A : Type) : IsEquiv idmap | 0 :=
+  BuildIsEquiv A A idmap idmap (fun _ => 1) (fun _ => 1) (fun _ => 1).
+
+Definition equiv_idmap (A : Type) : A <~> A := BuildEquiv A A idmap _.
+
+Arguments equiv_idmap {A} , A.
+
+Notation "1" := equiv_idmap : equiv_scope.
+
+Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g}
+  : IsEquiv (compose g f) | 1000
+  := BuildIsEquiv A C (compose g f)
+    (compose f^-1 g^-1)
+    (fun c => ap g (eisretr f (g^-1 c)) @ eisretr g c)
+    (fun a => ap (f^-1) (eissect g (f a)) @ eissect f a)
+    (fun a =>
+      (whiskerL _ (eisadj g (f a))) @
+      (ap_pp g _ _)^ @
+      ap02 g
+      ( (concat_A1p (eisretr f) (eissect g (f a)))^ @
+        (ap_compose f^-1 f _ @@ eisadj f a) @
+        (ap_pp f _ _)^
+      ) @
+      (ap_compose f g _)^
+    ).
+
+Definition equiv_compose {A B C : Type} (g : B -> C) (f : A -> B)
+  `{IsEquiv B C g} `{IsEquiv A B f}
+  : A <~> C
+  := BuildEquiv A C (compose g f) _.
+
+Global Instance transitive_equiv : Transitive Equiv | 0 :=
+  fun _ _ _ f g => equiv_compose g f.
+
+Theorem equiv_inverse {A B : Type} : (A <~> B) -> (B <~> A).
+admit.
+Defined.
+
+Global Instance symmetric_equiv : Symmetric Equiv | 0 := @equiv_inverse.
+
+End Equivalences.
+
+Definition path_prod_uncurried {A B : Type} (z z' : A * B)
+  (pq : (fst z = fst z') * (snd z = snd z'))
+  : (z = z').
+admit.
+Defined.
+
+Global Instance isequiv_path_prod {A B : Type} {z z' : A * B}
+: IsEquiv (path_prod_uncurried z z') | 0.
+admit.
+Defined.
+
+Definition equiv_path_prod {A B : Type} (z z' : A * B)
+  : (fst z = fst z') * (snd z = snd z')  <~>  (z = z')
+  := BuildEquiv _ _ (path_prod_uncurried z z') _.
+
+Generalizable Variables X A B C f g n.
+
+Definition functor_sigma `{P : A -> Type} `{Q : B -> Type}
+           (f : A -> B) (g : forall a, P a -> Q (f a))
+: sigT P -> sigT Q
+  := fun u => (f u.1 ; g u.1 u.2).
+
+Global Instance isequiv_functor_sigma `{P : A -> Type} `{Q : B -> Type}
+         `{IsEquiv A B f} `{forall a, @IsEquiv (P a) (Q (f a)) (g a)}
+: IsEquiv (functor_sigma f g) | 1000.
+admit.
+Defined.
+
+Definition equiv_functor_sigma `{P : A -> Type} `{Q : B -> Type}
+           (f : A -> B) `{IsEquiv A B f}
+           (g : forall a, P a -> Q (f a))
+           `{forall a, @IsEquiv (P a) (Q (f a)) (g a)}
+: sigT P <~> sigT Q
+  := BuildEquiv _ _ (functor_sigma f g) _.
+
+Definition equiv_functor_sigma' `{P : A -> Type} `{Q : B -> Type}
+           (f : A <~> B)
+           (g : forall a, P a <~> Q (f a))
+: sigT P <~> sigT Q
+  := equiv_functor_sigma f g.
+
+Definition equiv_functor_sigma_id `{P : A -> Type} `{Q : A -> Type}
+           (g : forall a, P a <~> Q a)
+: sigT P <~> sigT Q
+  := equiv_functor_sigma' 1 g.
+
+Definition Bip : Type := { C : Type &  C * C }.
+
+Definition BipMor (X Y : Bip) : Type :=
+  match X, Y with (C;(c0,c1)), (D;(d0,d1)) =>
+    { f : C -> D & (f c0 = d0) * (f c1 = d1) }
+  end.
+
+Definition bipmor2map {X Y : Bip} : BipMor X Y -> X.1 -> Y.1 :=
+  match X, Y with (C;(c0,c1)), (D;(d0,d1)) => fun i =>
+    match i with (f;_) => f end
+  end.
+
+Definition bipidmor {X : Bip} : BipMor X X :=
+  match X with (C;(c0,c1)) => (idmap; (1, 1)) end.
+
+Definition bipcompmor {X Y Z : Bip} : BipMor X Y -> BipMor Y Z -> BipMor X Z :=
+  match X, Y, Z with (C;(c0,c1)), (D;(d0,d1)), (E;(e0,e1)) => fun i j =>
+    match i, j with (f;(f0,f1)), (g;(g0,g1)) =>
+      (g o f; (ap g f0 @ g0, ap g f1 @ g1))
+    end
+  end.
+
+Definition isbipequiv {X Y : Bip} (i : BipMor X Y) : Type :=
+  { l : BipMor Y X & bipcompmor i l = bipidmor } *
+  { r : BipMor Y X & bipcompmor r i = bipidmor }.
+
+Lemma bipequivEQequiv : forall {X Y : Bip} (i : BipMor X Y),
+  isbipequiv i <~> IsEquiv (bipmor2map i).
+Proof.
+assert (equivcompmor : forall {X Y : Bip} (i : BipMor X Y) j,
+(bipcompmor i j = bipidmor) <~> Unit).
+  intros; set (U := X); set (V := Y); destruct X as [C [c0 c1]], Y as [D [d0 d1]].
+  transitivity { n : (bipcompmor i j).1 = (@bipidmor U).1 &
+  (bipcompmor i j).2 = transport (fun h => (h c0 = c0) * (h c1 = c1)) n^ (@bipidmor U).2}.
+    admit.
+  destruct i as [f [f0 f1]]; destruct j as [g [g0 g1]].
+
+  transitivity { n : g o f = idmap & (ap g f0 @ g0 = apD10 n c0 @ 1) *
+  (ap g f1 @ g1 = apD10 n c1 @ 1)}.
+    apply equiv_functor_sigma_id; intro n.
+    assert (Ggen : forall (h0 h1 : C -> C) (p : h0 = h1) u0 u1 v0 v1,
+    ((u0, u1) = transport (fun h => (h c0 = c0) * (h c1 = c1)) p^ (v0, v1)) <~>
+    (u0 = apD10 p c0 @ v0) * (u1 = apD10 p c1 @ v1)).
+      induction p; intros; simpl; rewrite !concat_1p; apply symmetry.
+      by apply (equiv_path_prod (u0,u1) (v0,v1)).
+    rapply Ggen.
+    pose (@paths C).
+    Check (@paths C).
+    Undo.
+    Check (@paths C). (* Toplevel input, characters 0-17:
+Error: Illegal application:
+The term "@paths" of type "forall A : Type, A -> A -> Type"
+cannot be applied to the term
+ "C" : "Type"
+This term has type "Type@{Top.892}" which should be coercible to
+ "Type@{Top.882}".
+*)
-- 
cgit v1.2.3


From d82f2c96e73484aae7e6f9e014823065584fbc6e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Feb 2015 09:21:21 +0100
Subject: Moving test for bug #3681 as closed.

---
 test-suite/bugs/closed/3681.v | 20 ++++++++++++++++++++
 test-suite/bugs/opened/3681.v | 20 --------------------
 2 files changed, 20 insertions(+), 20 deletions(-)
 create mode 100644 test-suite/bugs/closed/3681.v
 delete mode 100644 test-suite/bugs/opened/3681.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3681.v b/test-suite/bugs/closed/3681.v
new file mode 100644
index 0000000000..194113c6ed
--- /dev/null
+++ b/test-suite/bugs/closed/3681.v
@@ -0,0 +1,20 @@
+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/3681.v b/test-suite/bugs/opened/3681.v
deleted file mode 100644
index 194113c6ed..0000000000
--- 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.
-- 
cgit v1.2.3


From 9dacc590c604290d9556d9368c5c735321e01e90 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 26 Feb 2015 09:58:46 +0100
Subject: Revert "Fixing bug #4035 (support for dependent destruction within
 ltac code)."

This reverts commit 4e6c9891140932f452bb5ac8960d597b0b5fde1d, which was
breaking compatibility because one could no longer use names of foralls in
the goal without introducting them. Probably not good style, but it did
break many existing developments including CompCert.

Closes #4093 but reopens #4035.
---
 test-suite/bugs/closed/4035.v | 7 -------
 1 file changed, 7 deletions(-)
 delete mode 100644 test-suite/bugs/closed/4035.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/4035.v b/test-suite/bugs/closed/4035.v
deleted file mode 100644
index 24f340bbd9..0000000000
--- a/test-suite/bugs/closed/4035.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(* Use of dependent destruction from ltac *)
-Require Import Program.
-Goal nat -> Type.
-  intro x.
-  lazymatch goal with
-  | [ x : nat |- _ ] => dependent destruction x
-  end.
-- 
cgit v1.2.3


From bc7d29e4c0f53d5c8e654157c4137c7e82910a7a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Feb 2015 17:22:41 +0100
Subject: Test for bug #3298.

---
 test-suite/bugs/closed/3298.v | 21 +++++++++++++++++++++
 test-suite/bugs/opened/3298.v | 23 -----------------------
 2 files changed, 21 insertions(+), 23 deletions(-)
 create mode 100644 test-suite/bugs/closed/3298.v
 delete mode 100644 test-suite/bugs/opened/3298.v

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3298.v b/test-suite/bugs/closed/3298.v
new file mode 100644
index 0000000000..3a7de45670
--- /dev/null
+++ b/test-suite/bugs/closed/3298.v
@@ -0,0 +1,21 @@
+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.
+    solve [ eauto ].
+  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.
+    solve [ eauto ] .
+  Qed.
+End BenDelaware.
diff --git a/test-suite/bugs/opened/3298.v b/test-suite/bugs/opened/3298.v
deleted file mode 100644
index bce7c3f23b..0000000000
--- 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.
-- 
cgit v1.2.3