From 9eb2f7480de8ded94a1b96eb4f6cc16d19a8c14d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 23 Oct 2016 21:26:20 +0200
Subject: Clarifying the interpretation path for the "constr_with_binding"
 argument.

This fixes an inconsistency introduced in 554a6c806 (svn r12603) where
both interp_constr_with_bindings and interp_open_constr_with_bindings
were going through interp_open_constr (no type classes so as to not to
commit too early on irreversible choices, accepting unresolved holes).

We fix this by having interp_constr_with_bindings going to
interp_constr (using type classes and failing on unresolved evars).

The external impact is that any TACTIC EXTEND which refers to
constr_with_binding has now to decide whether it intends it to use
what the name suggest (using type classes and to fail if evars remain
unresolved), thus keeping constr_with_binding, or the actual behavior
which requires to use open_constr_with_bindings for strict
compatibility.
---
 CHANGES                       |  5 ++++-
 dev/doc/changes.txt           |  6 ++++++
 interp/stdarg.ml              |  2 ++
 interp/stdarg.mli             |  5 +++++
 plugins/ltac/coretactics.ml4  |  4 ++--
 plugins/ltac/extratactics.ml4 |  2 +-
 plugins/ltac/tacinterp.ml     | 18 ++++++++++++------
 7 files changed, 32 insertions(+), 10 deletions(-)

diff --git a/CHANGES b/CHANGES
index b5f6ba9279..207dc167fd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -22,13 +22,16 @@ Tactics
   beta-iota-reduced after type-checking. This has an impact on the
   type of the variables that the tactic "refine" introduces in the
   context, producing types a priori closer to the expectations.
+- In "Tactic Notation" or "TACTIC EXTEND", entry "constr_with_bindings"
+  now uses type classes and rejects terms with unresolved holes, like
+  entry "constr" does. To get the former behavior use
+  "open_constr_with_bindings" (possible source of incompatibility.
 
 Vernacular Commands
 
 - Goals context can be printed in a more compact way when "Set
   Printing Compact Contexts" is activated.
 
-
 Standard Library
 
 - New file PropExtensionality.v to explicitly work in the axiomatic
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 8ea1638c99..7db5647c30 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -93,6 +93,12 @@ alternative solution would be to fully qualify Ltac modules, e.g. turning any
 call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not
 work for EXTEND macros though.
 
+** Additional changes in tactic extensions **
+
+Entry "constr_with_bindings" has been renamed into
+"open_constr_with_bindings". New entry "constr_with_bindings" now
+uses type classes and rejects terms with unresolved holes.
+
 ** Error handling **
 
 - All error functions now take an optional parameter `?loc:Loc.t`. For
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 5920b0d508..64f8b3913e 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -59,6 +59,8 @@ let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
 
 let wit_constr_with_bindings = make0 "constr_with_bindings"
 
+let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
+
 let wit_bindings = make0 "bindings"
 
 let wit_red_expr = make0 "redexpr"
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index ac40a23281..893ec54d45 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -59,6 +59,11 @@ val wit_constr_with_bindings :
   glob_constr_and_expr with_bindings,
   constr with_bindings delayed_open) genarg_type
 
+val wit_open_constr_with_bindings :
+  (constr_expr with_bindings,
+  glob_constr_and_expr with_bindings,
+  constr with_bindings delayed_open) genarg_type
+
 val wit_bindings :
   (constr_expr bindings,
   glob_constr_and_expr bindings,
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 28ff6df838..2d1220385a 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -141,10 +141,10 @@ END
 (** Specialize *)
 
 TACTIC EXTEND specialize
-  [ "specialize" constr_with_bindings(c) ] -> [
+  [ "specialize" open_constr_with_bindings(c) ] -> [
     Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None)
   ]
-| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [
+| [ "specialize" open_constr_with_bindings(c) "as" intropattern(ipat) ] -> [
     Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat))
   ]
 END
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index bd48614dbc..a3b3fae0b3 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -190,7 +190,7 @@ let onSomeWithHoles tac = function
   | Some c -> Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> tac (Some c))
 
 TACTIC EXTEND contradiction
- [ "contradiction" constr_with_bindings_opt(c) ] ->
+ [ "contradiction" open_constr_with_bindings_opt(c) ] ->
     [ onSomeWithHoles contradiction c ]
 END
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index b8c021f188..051cd31b2b 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -996,7 +996,7 @@ let interp_bindings ist env sigma = function
 
 let interp_constr_with_bindings ist env sigma (c,bl) =
   let sigma, bl = interp_bindings ist env sigma bl in
-  let sigma, c = interp_open_constr ist env sigma c in
+  let sigma, c = interp_constr ist env sigma c in
   sigma, (c,bl)
 
 let interp_open_constr_with_bindings ist env sigma (c,bl) =
@@ -1025,7 +1025,7 @@ let interp_destruction_arg ist gl arg =
   | keep,ElimOnConstr c ->
       keep,ElimOnConstr { delayed = fun env sigma ->
         let sigma = Sigma.to_evar_map sigma in
-        let (sigma, c) = interp_constr_with_bindings ist env sigma c in
+        let (sigma, c) = interp_open_constr_with_bindings ist env sigma c in
         Sigma.Unsafe.of_pair (c, sigma)
       }
   | keep,ElimOnAnonHyp n as x -> x
@@ -1678,8 +1678,8 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in 
-        let sigma, cb = interp_constr_with_bindings ist env sigma cb in
-        let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
+        let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
+        let sigma, cbo = Option.fold_map (interp_open_constr_with_bindings ist env) sigma cbo in
         let named_tac =
           let tac = Tactics.elim ev keep cb cbo in
           name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac
@@ -1690,7 +1690,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.Goal.enter { enter = begin fun gl ->
         let sigma = project gl in
         let env = Proofview.Goal.env gl in
-        let sigma, cb = interp_constr_with_bindings ist env sigma cb in
+        let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
         let named_tac =
           let tac = Tactics.general_case_analysis ev keep cb in
           name_atomic ~env (TacCase(ev,(keep,cb))) tac
@@ -1807,7 +1807,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         let l,lp = List.split l in
         let sigma,el =
-          Option.fold_map (interp_constr_with_bindings ist env) sigma el in
+          Option.fold_map (interp_open_constr_with_bindings ist env) sigma el in
         let tac = name_atomic ~env
           (TacInductionDestruct(isrec,ev,(lp,el)))
             (Tactics.induction_destruct isrec ev (l,el))
@@ -2045,6 +2045,11 @@ let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigm
   Sigma.Unsafe.of_pair (c, sigma)
   }
 
+let interp_open_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigma ->
+  let (sigma, c) = interp_open_constr_with_bindings ist env (Sigma.to_evar_map sigma) c in
+  Sigma.Unsafe.of_pair (c, sigma)
+  }
+
 let interp_destruction_arg' ist c = Ftactic.enter { enter = begin fun gl ->
   Ftactic.return (interp_destruction_arg ist gl c)
 end }
@@ -2067,6 +2072,7 @@ let () =
   register_interp0 wit_open_constr (lifts interp_open_constr);
   register_interp0 wit_bindings interp_bindings';
   register_interp0 wit_constr_with_bindings interp_constr_with_bindings';
+  register_interp0 wit_open_constr_with_bindings interp_open_constr_with_bindings';
   register_interp0 wit_destruction_arg interp_destruction_arg';
   ()
 
-- 
cgit v1.2.3


From 9f463c144c54a013a0ee214383391f9fc48259d9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Oct 2016 11:29:52 +0200
Subject: Using type classes in the interpretation of "specialize" and
 "contradiction".

We do that by using constr_with_bindings rather than
open_constr_with_bindings (+ extra call to typeclasses in
"specialize"). If my understanding is right, the only effect would be
to succeed more in cases where it was failing (in
inh_conv_coerce_to_gen). In particular, "specialize" and
"contradiction" already have a WITHHOLES test for rejecting pending
holes.

Incidentally, this answers enhancement #5153.
---
 plugins/ltac/coretactics.ml4    | 4 ++--
 plugins/ltac/extratactics.ml4   | 2 +-
 tactics/tactics.ml              | 4 ----
 test-suite/bugs/closed/5153.v   | 8 ++++++++
 test-suite/success/specialize.v | 8 ++++++++
 5 files changed, 19 insertions(+), 7 deletions(-)
 create mode 100644 test-suite/bugs/closed/5153.v

diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 2d1220385a..28ff6df838 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -141,10 +141,10 @@ END
 (** Specialize *)
 
 TACTIC EXTEND specialize
-  [ "specialize" open_constr_with_bindings(c) ] -> [
+  [ "specialize" constr_with_bindings(c) ] -> [
     Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None)
   ]
-| [ "specialize" open_constr_with_bindings(c) "as" intropattern(ipat) ] -> [
+| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [
     Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat))
   ]
 END
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index a3b3fae0b3..bd48614dbc 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -190,7 +190,7 @@ let onSomeWithHoles tac = function
   | Some c -> Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> tac (Some c))
 
 TACTIC EXTEND contradiction
- [ "contradiction" open_constr_with_bindings_opt(c) ] ->
+ [ "contradiction" constr_with_bindings_opt(c) ] ->
     [ onSomeWithHoles contradiction c ]
 END
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 15cef676e6..e41236b1c3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2966,10 +2966,6 @@ let specialize (c,lbind) ipat =
   let env = Proofview.Goal.env gl in
   let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
   let sigma, term =
-    if lbind == NoBindings then
-      let sigma = Typeclasses.resolve_typeclasses env sigma in
-      sigma, nf_evar sigma c
-    else
       let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma c) lbind in
       let flags = { (default_unify_flags ()) with resolve_evars = true } in
       let clause = clenv_unify_meta_types ~flags clause in
diff --git a/test-suite/bugs/closed/5153.v b/test-suite/bugs/closed/5153.v
new file mode 100644
index 0000000000..be6407b5fa
--- /dev/null
+++ b/test-suite/bugs/closed/5153.v
@@ -0,0 +1,8 @@
+(* An example where it does not hurt having more type-classes resolution *)
+Class some_type := { Ty : Type }.
+Instance: some_type := { Ty := nat }.
+Arguments Ty : clear implicits.
+Goal forall (H : forall t : some_type, @Ty t -> False) (H' : False -> 1 = 2), 1 = 2.
+Proof.
+intros H H'.
+specialize (H' (@H _ O)). (* was failing *)
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index fba05cd902..4b41a509e5 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -72,3 +72,11 @@ intros.
 specialize (H 1) as ->.
 reflexivity.
 Qed.
+
+(* A test from corn *)
+
+Goal (forall x y, x=0 -> y=0 -> True) -> True.
+intros.
+specialize (fun z => H 0 z eq_refl).
+exact (H 0 eq_refl).
+Qed.
-- 
cgit v1.2.3


From 5c5f7c8d6a6ed8cbb99b12dde09fdbcc30ca8ab9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 22 May 2017 12:15:21 +0200
Subject: Compatibility fix while waiting for integration of Pierre Courtieu's
 PR #449.

---
 tactics/tactics.ml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e41236b1c3..fd10c622a0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2966,6 +2966,9 @@ let specialize (c,lbind) ipat =
   let env = Proofview.Goal.env gl in
   let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
   let sigma, term =
+    if lbind == NoBindings then
+      sigma, c
+    else
       let clause = make_clenv_binding env sigma (c,Retyping.get_type_of env sigma c) lbind in
       let flags = { (default_unify_flags ()) with resolve_evars = true } in
       let clause = clenv_unify_meta_types ~flags clause in
-- 
cgit v1.2.3