diff options
Diffstat (limited to 'contrib/subtac/g_subtac.ml4')
| -rw-r--r-- | contrib/subtac/g_subtac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 933ea94b31..d589c5c1f6 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -112,7 +112,7 @@ VERNAC COMMAND EXTEND Subtac_Solve_Obligations END VERNAC COMMAND EXTEND Subtac_Set_Solver -| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.interp t) ] +| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.glob_tactic t) ] END VERNAC COMMAND EXTEND Subtac_Show_Obligations |