X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.mli;h=34abacfde29654e602c12262fc2b046ef30dec65;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=a0c9272845e9fbd29d58d29e5104a8db5796a556;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_kernel/nCicTypeChecker.mli b/matita/components/ng_kernel/nCicTypeChecker.mli
index a0c927284..34abacfde 100644
--- a/matita/components/ng_kernel/nCicTypeChecker.mli
+++ b/matita/components/ng_kernel/nCicTypeChecker.mli
@@ -26,19 +26,21 @@ val set_logger:
 val set_trust : (NCic.obj -> bool) -> unit
 
 val typeof: 
-  subst:NCic.substitution -> metasenv:NCic.metasenv -> 
-  NCic.context -> NCic.term -> 
-    NCic.term
+ #NCic.status -> subst:NCic.substitution -> metasenv:NCic.metasenv -> 
+  NCic.context -> NCic.term -> NCic.term
 
-val height_of_obj_kind: NUri.uri -> subst:NCic.substitution -> NCic.obj_kind -> int
+val height_of_obj_kind:
+ #NCic.status -> NUri.uri -> subst:NCic.substitution -> NCic.obj_kind -> int
 
 val get_relevance : 
+ #NCic.status ->
   metasenv:NCic.metasenv -> subst:NCic.substitution ->
   NCic.context -> NCic.term -> NCic.term list -> bool list
 
 (* type_of_branch subst context leftno outtype 
  *   (constr @ lefts) (ty_constr @ lefts)  *)
 val type_of_branch : 
+ #NCic.status ->
   subst:NCic.substitution ->
     NCic.context -> int -> NCic.term -> NCic.term -> NCic.term -> 
      NCic.term
@@ -47,6 +49,7 @@ val type_of_branch :
  * arity1 = constructor type @ lefts
  * arity2 = outtype *)
 val check_allowed_sort_elimination : 
+ #NCic.status ->
   subst:NCic.substitution ->
   metasenv:NCic.metasenv ->
   NReference.reference -> NCic.context -> 
@@ -54,11 +57,17 @@ val check_allowed_sort_elimination :
 
 (* Functions to be used by the refiner *)
 val debruijn:
- NUri.uri -> int -> subst:NCic.substitution -> NCic.context -> NCic.term ->
-  NCic.term
+ #NCic.status -> NUri.uri -> int -> subst:NCic.substitution -> NCic.context ->
+  NCic.term -> NCic.term
+
 val are_all_occurrences_positive: 
- subst:NCic.substitution ->
-  NCic.context -> NUri.uri -> int -> int -> int -> int -> NCic.term -> bool
+ #NCic.status -> subst:NCic.substitution -> NCic.context -> NUri.uri -> int ->
+  int -> int -> int -> NCic.term -> bool
 
+(* does_not_occur ... n nn t
+ * detects the Rels m of t in the range n < m <= nn
+ * recursively delta-expanding the Rels m of t in the range 0 < m <= n
+ *)
 val does_not_occur :
-    subst:NCic.substitution -> NCic.context -> int -> int -> NCic.term -> bool
+ #NCic.status -> subst:NCic.substitution -> NCic.context -> int -> int ->
+  NCic.term -> bool