From 95354e0dee4832c22cdcbf12f257e829ce7d9d29 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Thu, 3 Dec 2015 17:02:29 +0100 Subject: [PATCH] Removing the only use of globTacticIn. --- mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index 67f370e69b..e05526e1cd 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 @@ -1043,10 +1043,7 @@ let ssrtac_expr = ssrtac_atom let ssrevaltac ist gtac = - let debug = match TacStore.get ist.extra f_debug with - | None -> Tactic_debug.DebugOff | Some level -> level - in - Proofview.V82.of_tactic (interp_tac_gen ist.lfun [] debug (globTacticIn (fun _ -> gtac))) + Proofview.V82.of_tactic (eval_tactic_ist ist gtac) (* fun gl -> let lfun = [tacarg_id, val_interp ist gl gtac] in interp_tac_gen lfun [] ist.debug tacarg_expr gl *)