From ec8523065abfb68aff9bd3664869224419885385 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Jun 2017 06:54:07 +0200 Subject: [vernac] Remove forward hooks from Obligations. This was (once again) a spurious inter-dependency, that we solve by introducing a new module with the proper functionality. This helps in cleaning up the code. Note that no code was changed, other than removing the setting of the references. --- vernac/obligations.ml | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) (limited to 'vernac/obligations.ml') diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 135e4c63a..c0acdaf57 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -22,9 +22,6 @@ open Util module NamedDecl = Context.Named.Declaration -let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false) -let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false) - let get_fix_exn, stm_get_fix_exn = Hook.make () let succfix (depth, fixrels) = @@ -496,14 +493,12 @@ let declare_definition prg = in let () = progmap_remove prg in let cst = - !declare_definition_ref prg.prg_name - prg.prg_kind ce prg.prg_implicits + DeclareDef.declare_definition prg.prg_name + prg.prg_kind ce [] prg.prg_implicits (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) in Universes.register_universe_binders cst pl; cst - -open Pp let rec lam_index n t acc = match kind_of_term t with @@ -569,7 +564,7 @@ let declare_mutual_definition l = (* Declare the recursive definitions *) let ctx = Evd.evar_context_universe_context first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx) + let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) [] ctx) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter Metasyntax.add_notation_interpretation first.prg_notations; -- cgit v1.2.3