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.

3 files changed, 15 insertions, 9 deletions

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';
   ()