]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/ng_kernel/nCicTypeChecker.mli
This commit patches the environment and the library so that their status is
[helm.git] / matitaB / components / ng_kernel / nCicTypeChecker.mli
index 6ca329fbff1c9f97e81dedec445080fae5db5d5b..cbbc770f035db120ccd6a26bc47962a724df5d6d 100644 (file)
@@ -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