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/classes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/classes.ml')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 007b70bc0f..2e8ebb8531 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -417,7 +417,7 @@ let context poly l =
         let decl = (Discharge, poly, Definition) in
         let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
         let hook = Lemmas.mk_hook (fun _ gr -> gr) in
-        let _ = Command.declare_definition id decl entry [] [] hook in
+        let _ = DeclareDef.declare_definition id decl entry [] [] hook in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
 	status && nstatus
-- 
cgit v1.2.3