aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--tactics/tactics.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fe3854143..8546b03a1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3897,10 +3897,10 @@ let unify ?(state=full_transparent_state) x y gl =
in tclEVARS evd gl
with e when Errors.noncritical e -> tclFAIL 0 (str"Not unifiable") gl
-let emit_side_effects eff gl =
- Declareops.iter_side_effects (fun e ->
+let emit_side_effects eff gl =
+(* Declareops.iter_side_effects (fun e ->
prerr_endline ("emitting: " ^ Declareops.string_of_side_effect e))
- eff;
+ eff; *)
{ it = [gl.it] ; sigma = Evd.emit_side_effects eff gl.sigma; }
module Simple = struct