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/funind/functional_principles_types.ml | 17 ++++++++---------
 plugins/funind/recdef.ml                      |  4 +++-
 plugins/setoid_ring/newring.ml4               |  4 +++-
 3 files changed, 14 insertions(+), 11 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 2661a78a5a..56b1a3f1cb 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -339,15 +339,14 @@ let generate_functional_principle
 	let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
 	let value = change_property_sort s new_principle_type new_princ_name in
 	(*       Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-	let ce =
-          { const_entry_body =
-              Future.from_val (value,Declareops.no_seff);
-            const_entry_secctx = None;
-	    const_entry_type = None;
-	    const_entry_opaque = false;
-	    const_entry_inline_code = false
-	  }
-	in
+	let ce = {
+          const_entry_body = Future.from_val (value,Declareops.no_seff);
+          const_entry_secctx = None;
+          const_entry_type = None;
+          const_entry_opaque = false;
+          const_entry_inline_code = false;
+          const_entry_feedback = None;
+	} in
 	ignore(
 	  Declare.declare_constant
 	    name
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 082d7ad51e..26e1011ba1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -61,7 +61,9 @@ let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) =
               const_entry_secctx = None;
 	      const_entry_type = None;
           const_entry_opaque = false;
-          const_entry_inline_code = false} in
+          const_entry_inline_code = false;
+          const_entry_feedback = None;
+    } in
       ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
 
 let defined () = Lemmas.save_proof (Vernacexpr.Proved (false,None))
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