diff options
| author | Pierre-Marie Pédrot | 2015-12-03 17:02:29 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-12-03 19:51:38 +0100 |
| commit | 95354e0dee4832c22cdcbf12f257e829ce7d9d29 (patch) | |
| tree | 5e4898940520e7c42bcdd148c0ec12fff9130afe | |
| parent | 7bf7dca588710bba38a173dedb2a3cb7408c1b2a (diff) | |
Removing the only use of globTacticIn.
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index 67f370e..e05526e 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 *) |