diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_obligations.mlg | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 498b33d1a8..81ee6ed5bb 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -28,7 +28,7 @@ let () = let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> snd (get_default_tactic ()) end in - Obligations.default_tactic := tac + Declare.Obls.default_tactic := tac let with_tac f tac = let env = Genintern.empty_glob_sign (Global.env ()) in @@ -78,10 +78,10 @@ GRAMMAR EXTEND Gram { -open Obligations +open Declare.Obls -let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac -let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac +let obligation obl tac = with_tac (fun t -> obligation obl t) tac +let next_obligation obl tac = with_tac (fun t -> next_obligation obl t) tac let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[])) |