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 51e1a1709..337cd1696 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -140,7 +140,7 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations VERNAC COMMAND EXTEND Subtac_Set_Solver | [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ - Subtac.require_library "Coq.Program.Tactics"; + Coqlib.check_required_library ["Coq";"Program";"Tactics"]; Tacinterp.add_tacdef false [((dummy_loc, id_of_string "obligations_tactic"), true, t)] ] END |