From 18c7a10341b462256b576542412db889d528465f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 24 Dec 2013 18:18:10 +0100
Subject: Qed: feedback when type checking is done

To make this possible the state id has to reach the kernel.
Hence definition_entry has an extra field, and many files had
to be fixed.
---
 plugins/setoid_ring/newring.ml4 | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins/setoid_ring')

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index aee7efb76d..b8507041f3 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -152,7 +152,9 @@ let decl_constant na c =
       const_entry_secctx = None;
       const_entry_type = None;
       const_entry_opaque = true;
-      const_entry_inline_code = false},
+      const_entry_inline_code = false;
+      const_entry_feedback = None;
+    },
     IsProof Lemma))
 
 (* Calling a global tactic *)
-- 
cgit v1.2.3