Code extraction branched.

[helm.git] / matita / components / ng_kernel / nCicEnvironment.mli

diff --git a/matita/components/ng_kernel/nCicEnvironment.mli b/matita/components/ng_kernel/nCicEnvironment.mli
index 80fcd2b68e4f993c3e49adfe2fe6c7c115df7399..a557ef563b0b922b6bb6424adf8d26382b61992a 100644 (file)
--- a/matita/components/ng_kernel/nCicEnvironment.mli
+++ b/matita/components/ng_kernel/nCicEnvironment.mli
@@ -24,6 +24,10 @@ val check_and_add_obj: #NCic.status -> NCic.obj -> unit
 
 val get_relevance: #NCic.status -> NReference.reference -> bool list
 
+val get_checked_decl:
+  #NCic.status -> NReference.reference -> 
+    NCic.relevance * string * NCic.term * NCic.c_attr * int
+
 val get_checked_def:
   #NCic.status -> NReference.reference -> 
     NCic.relevance * string * NCic.term * NCic.term * NCic.c_attr * int