X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.mli;h=cbbc770f035db120ccd6a26bc47962a724df5d6d;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hp=6ca329fbff1c9f97e81dedec445080fae5db5d5b;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/ng_kernel/nCicTypeChecker.mli b/matitaB/components/ng_kernel/nCicTypeChecker.mli
index 6ca329fbf..cbbc770f0 100644
--- a/matitaB/components/ng_kernel/nCicTypeChecker.mli
+++ b/matitaB/components/ng_kernel/nCicTypeChecker.mli
@@ -26,21 +26,21 @@ val set_logger:
 val set_trust : (NCic.obj -> bool) -> unit
 
 val typeof: 
- #NCic.status -> subst:NCic.substitution -> metasenv:NCic.metasenv -> 
+  #NCicEnvironment.status -> subst:NCic.substitution -> metasenv:NCic.metasenv -> 
   NCic.context -> NCic.term -> NCic.term
 
 val height_of_obj_kind:
- #NCic.status -> NUri.uri -> subst:NCic.substitution -> NCic.obj_kind -> int
+ #NCicEnvironment.status -> NUri.uri -> subst:NCic.substitution -> NCic.obj_kind -> int
 
 val get_relevance : 
- #NCic.status ->
+ #NCicEnvironment.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 ->
+ #NCicEnvironment.status ->
   subst:NCic.substitution ->
     NCic.context -> int -> NCic.term -> NCic.term -> NCic.term -> 
      NCic.term
@@ -49,7 +49,7 @@ val type_of_branch :
  * arity1 = constructor type @ lefts
  * arity2 = outtype *)
 val check_allowed_sort_elimination : 
- #NCic.status ->
+ #NCicEnvironment.status ->
   subst:NCic.substitution ->
   metasenv:NCic.metasenv ->
   NReference.reference -> NCic.context -> 
@@ -57,13 +57,13 @@ val check_allowed_sort_elimination :
 
 (* Functions to be used by the refiner *)
 val debruijn:
- #NCic.status -> NUri.uri -> int -> subst:NCic.substitution -> NCic.context ->
+ #NCicEnvironment.status -> NUri.uri -> int -> subst:NCic.substitution -> NCic.context ->
   NCic.term -> NCic.term
 
 val are_all_occurrences_positive: 
- #NCic.status -> subst:NCic.substitution -> NCic.context -> NUri.uri -> int ->
+ #NCicEnvironment.status -> subst:NCic.substitution -> NCic.context -> NUri.uri -> int ->
   int -> int -> int -> NCic.term -> bool
 
 val does_not_occur :
- #NCic.status -> subst:NCic.substitution -> NCic.context -> int -> int ->
+ #NCicEnvironment.status -> subst:NCic.substitution -> NCic.context -> int -> int ->
   NCic.term -> bool