diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-09 23:45:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-09 23:46:51 +0100 |
| commit | 9fa45b3b3b67cf98abb3c246880b2c202c475947 (patch) | |
| tree | 16fd35d7ea6ac83fd3d57a6bb551ba77878d51c7 /tactics | |
| parent | 03b0c585e2b4946be6c529eb3359c3715ea312cb (diff) | |
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.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e16b9973f..fa1683070 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) -> |