From cedcfc9bc386456f3fdd225f739706e4f7a2902c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 15 Dec 2015 10:51:08 +0100
Subject: Refine tactic now shelves unifiable holes.

The unshelve tactical can be used to get the shelved holes. This changes the
proper ordering of holes though, so expect some broken scripts. Also, the
test-suite is not fixed yet.
---
 test-suite/bugs/closed/3685.v |  4 ++--
 test-suite/bugs/closed/3686.v |  4 ++--
 test-suite/bugs/closed/3699.v | 16 ++++++++--------
 3 files changed, 12 insertions(+), 12 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3685.v b/test-suite/bugs/closed/3685.v
index a5bea34a98..7a0c3e6f1d 100644
--- a/test-suite/bugs/closed/3685.v
+++ b/test-suite/bugs/closed/3685.v
@@ -39,11 +39,11 @@ Module Export PointwiseCore.
              (G : Functor D D')
   : Functor (C -> D) (C' -> D').
   Proof.
-    refine (Build_Functor
+    unshelve (refine (Build_Functor
               (C -> D) (C' -> D')
               _
               _
-              _);
+              _));
     abstract admit.
   Defined.
 End PointwiseCore.
diff --git a/test-suite/bugs/closed/3686.v b/test-suite/bugs/closed/3686.v
index b650920b26..df5f667480 100644
--- a/test-suite/bugs/closed/3686.v
+++ b/test-suite/bugs/closed/3686.v
@@ -33,11 +33,11 @@ Module Export PointwiseCore.
              (G : Functor D D')
   : Functor (C -> D) (C' -> D').
   Proof.
-    refine (Build_Functor
+    unshelve (refine (Build_Functor
               (C -> D) (C' -> D')
               _
               _
-              _);
+              _));
     abstract admit.
   Defined.
 End PointwiseCore.
diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v
index 62137f0c06..aad0bb44d5 100644
--- a/test-suite/bugs/closed/3699.v
+++ b/test-suite/bugs/closed/3699.v
@@ -34,8 +34,8 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -47,8 +47,8 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intros [a p].
     exact (transport P p (d a)).
   Defined.
@@ -111,8 +111,8 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -124,8 +124,8 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intros [a p].
     exact (transport P p (d a)).
   Defined.
-- 
cgit v1.2.3


From a110ddfd6fc040a805de3f0ec2995b51ff301f5c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 15 Dec 2015 11:31:13 +0100
Subject: Adding a test for the unshelve tactical.

---
 test-suite/success/unshelve.v | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 test-suite/success/unshelve.v

(limited to 'test-suite')

diff --git a/test-suite/success/unshelve.v b/test-suite/success/unshelve.v
new file mode 100644
index 0000000000..672222bdd6
--- /dev/null
+++ b/test-suite/success/unshelve.v
@@ -0,0 +1,11 @@
+Axiom F : forall (b : bool), b = true ->
+  forall (i : unit), i = i -> True.
+
+Goal True.
+Proof.
+unshelve (refine (F _ _ _ _)).
++ exact true.
++ exact tt.
++ exact (@eq_refl bool true).
++ exact (@eq_refl unit tt).
+Qed.
-- 
cgit v1.2.3


From 34ea06f2f31cebf00bc7620fac34d963afe6a1dc Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 15 Dec 2015 14:54:07 +0100
Subject: Fix test-suite files after change in refine tactic.

Change was introduced by cedcfc9bc386456f3fdd225f739706e4f7a2902c.
---
 test-suite/bugs/closed/4116.v         | 6 +++---
 test-suite/bugs/closed/931.v          | 2 +-
 test-suite/bugs/closed/HoTT_coq_090.v | 2 +-
 test-suite/success/refine.v           | 2 +-
 4 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4116.v b/test-suite/bugs/closed/4116.v
index f808cb45e9..5932c9c56e 100644
--- a/test-suite/bugs/closed/4116.v
+++ b/test-suite/bugs/closed/4116.v
@@ -110,7 +110,7 @@ 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 _);
+  unshelve refine (let __transparent_assert_hypothesis := (_ : type) in _);
   [
       | (
         let H := match goal with H := _ |- _ => constr:(H) end in
@@ -321,7 +321,7 @@ Section Grothendieck.
 
   Definition Gcategory : PreCategory.
   Proof.
-    refine (@Build_PreCategory
+    unshelve refine (@Build_PreCategory
               Pair
               (fun s d => Gmorphism s d)
               Gidentity
@@ -346,7 +346,7 @@ Section Grothendieck2.
   Instance iscategory_grothendieck_toset : IsCategory (Gcategory F).
   Proof.
     intros s d.
-    refine (isequiv_adjointify _ _ _ _).
+    unshelve refine (isequiv_adjointify _ _ _ _).
     {
       intro m.
       transparent assert (H' : (s.(c) = d.(c))).
diff --git a/test-suite/bugs/closed/931.v b/test-suite/bugs/closed/931.v
index e86b3be64e..ea3347a851 100644
--- a/test-suite/bugs/closed/931.v
+++ b/test-suite/bugs/closed/931.v
@@ -2,6 +2,6 @@ Parameter P : forall n : nat, n=n -> Prop.
 
 Goal Prop.
   refine (P _ _).
-  2:instantiate (1:=0).
+    instantiate (1:=0).
   trivial.
 Qed.
diff --git a/test-suite/bugs/closed/HoTT_coq_090.v b/test-suite/bugs/closed/HoTT_coq_090.v
index 5fa167038d..d77b9b63a2 100644
--- a/test-suite/bugs/closed/HoTT_coq_090.v
+++ b/test-suite/bugs/closed/HoTT_coq_090.v
@@ -84,7 +84,7 @@ Arguments transport {A} P {x y} p%path_scope u : simpl nomatch.
 Instance isequiv_path {A B : Type} (p : A = B)
   : IsEquiv (transport (fun X:Type => X) p) | 0.
 Proof.
-  refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _);
+  unshelve refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _);
   admit.
 Defined.
 
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index 1e667884b8..352abb2af5 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -62,7 +62,7 @@ Abort.
 Goal (forall n : nat, n = 0 -> Prop) -> Prop.
 intro P.
  refine (P _ _).
-2:reflexivity.
+reflexivity.
 Abort.
 
 (* Submitted by Jacek Chrzaszcz (bug #1102) *)
-- 
cgit v1.2.3


From 0a89d4805a29628c82b994958362dc9d92709020 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 15 Dec 2015 18:56:08 +0100
Subject: Extraction: more cautious use of intermediate result caching (fix
 #3923)

 During an extraction, a few tables are maintained to cache
 intermediate results. Due to modules, the kernel_name index
 for these caching tables aren't enough. For instance, in
 bug #3923, a constant is first transparent (from inside the
 module) then opaque (when seen from the signature). The previous
 protections were actually obsolete (tests via visible_con), we
 now checks that the constant_body is still the same.
---
 test-suite/bugs/closed/3923.v | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 test-suite/bugs/closed/3923.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3923.v b/test-suite/bugs/closed/3923.v
new file mode 100644
index 0000000000..0aa029e73d
--- /dev/null
+++ b/test-suite/bugs/closed/3923.v
@@ -0,0 +1,33 @@
+Module Type TRIVIAL.
+Parameter t:Type.
+End TRIVIAL.
+
+Module MkStore (Key : TRIVIAL).
+
+Module St : TRIVIAL.
+Definition t := unit.
+End St.
+
+End MkStore.
+
+
+
+Module Type CERTRUNTIMETYPES (B  : TRIVIAL).
+
+Parameter cert_fieldstore : Type.
+Parameter empty_fieldstore : cert_fieldstore.
+
+End CERTRUNTIMETYPES.
+
+
+
+Module MkCertRuntimeTypes (B  : TRIVIAL) : CERTRUNTIMETYPES B.
+
+Module FieldStore := MkStore B.
+
+Definition cert_fieldstore := FieldStore.St.t.
+Axiom empty_fieldstore : cert_fieldstore.
+
+End MkCertRuntimeTypes.
+
+Extraction MkCertRuntimeTypes. (* Was leading to an uncaught Not_found *)
-- 
cgit v1.2.3


From 7212e6c4a742110138a268650a59a67ef28d0582 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 15 Dec 2015 21:15:42 +0100
Subject: Fix test suite after change in extraction.

---
 test-suite/output/Extraction_matchs_2413.out | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Extraction_matchs_2413.out b/test-suite/output/Extraction_matchs_2413.out
index 848abd0096..f738b0d091 100644
--- a/test-suite/output/Extraction_matchs_2413.out
+++ b/test-suite/output/Extraction_matchs_2413.out
@@ -4,7 +4,7 @@ let test1 b =
   b
 (** val test2 : bool -> bool **)
 
-let test2 b =
+let test2 _ =
   False
 (** val wrong_id : 'a1 hole -> 'a2 hole **)
 
-- 
cgit v1.2.3


From 33742251e62a49c7996b96ca7077cf985627d14b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 15 Dec 2015 23:15:02 +0100
Subject: Proof using: do not clear unused section hyps automatically

The option is still there, but not documented since it is too
dangerous.  Hints and type classes instances are not taking cleared
variables into account.
---
 test-suite/success/proof_using.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index c83f45e2a4..adaa05ad06 100644
--- a/test-suite/success/proof_using.v
+++ b/test-suite/success/proof_using.v
@@ -178,6 +178,7 @@ End Let.
 
 Check (test_let 3).
 
+(* Disabled
 Section Clear.
 
 Variable a: nat.
@@ -192,6 +193,6 @@ trivial.
 Qed.
 
 End Clear.
-
+*)
 
 
-- 
cgit v1.2.3