From 9fa45b3b3b67cf98abb3c246880b2c202c475947 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 9 Nov 2014 23:45:55 +0100
Subject: Fixing bug #3803.

The Info layer was setting the required evarmap too eagerly, making the
tclWITHHOLE tactical accept terms with holes. The logging facility is
now inside the tclWITHHOLES.
---
 tactics/tacinterp.ml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e16b9973f4..fa1683070c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2051,12 +2051,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
-        Proofview.Unsafe.tclEVARS sigma <*>
-        name_atomic ~env
-          (TacSplit (ev,bll))
-          (Tacticals.New.tclWITHHOLES ev
-             (Tactics.split_with_bindings ev)
-             sigma bll)
+        let tac bll =
+          let tac = Tactics.split_with_bindings ev bll in
+          name_atomic ~env (TacSplit (ev, bll)) tac
+        in
+        Tacticals.New.tclWITHHOLES ev tac sigma bll
       end
   (* Conversion *)
   | TacReduce (r,cl) ->
-- 
cgit v1.2.3