Removing the only use of globTacticIn.

math-comp · Dec 3, 2015 · 95354e0 · 95354e0
1 parent 7bf7dca
commit 95354e0
Showing 1 changed file with 1 addition and 4 deletions.
diff --git 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 *)