diff options
| author | Emilio Jesus Gallego Arias | 2020-06-23 22:36:22 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:13 +0200 |
| commit | 4a2c8653c0b2f5e73db769a8ea6bf79b76086524 (patch) | |
| tree | 0c1013329f008ef645c7b7712ccf55be72d39c25 /plugins/ltac | |
| parent | 06159c53e84ab1cff0299890767576972eaf83c2 (diff) | |
[declare] Merge remaining obligations bits into Declare
This allows us to remove a large chunk of the internal API, and is the
pre-requisite to get rid of [Proof_ending], and even more refactoring
on the declare path.
Diffstat (limited to 'plugins/ltac')
| -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,[])) |