X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.mli;h=6894129c86e5c5b2184544872a4af7252b0477ec;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hp=c9530d42da7305a03dbea015af841c65e97012e9;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/ng_refiner/nCicMetaSubst.mli b/matitaB/components/ng_refiner/nCicMetaSubst.mli
index c9530d42d..6894129c8 100644
--- a/matitaB/components/ng_refiner/nCicMetaSubst.mli
+++ b/matitaB/components/ng_refiner/nCicMetaSubst.mli
@@ -35,7 +35,7 @@ val maxmeta: unit -> int
  * in the term (for occur check).
  *)
 val delift : 
-  #NCic.status ->
+  #NCicEnvironment.status ->
   unify:(NCic.metasenv -> NCic.substitution -> NCic.context ->
     NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) -> 
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
@@ -47,7 +47,7 @@ val delift :
    additional (i.e. l' does not intersects l) positions whose restriction was
    forced because of type dependencies *)
 val restrict: 
-   #NCic.status ->
+   #NCicEnvironment.status ->
     NCic.metasenv ->
     NCic.substitution ->
     int -> int list ->
@@ -65,7 +65,7 @@ val extend_meta: NCic.metasenv -> int -> NCic.metasenv * NCic.term
 
 (* returns the resulting type, the metasenv and the arguments *)
 val saturate:
-   #NCic.status ->
+   #NCicEnvironment.status ->
     ?delta:int -> NCic.metasenv -> NCic.substitution -> 
     NCic.context -> NCic.term -> int ->
        NCic.term * NCic.metasenv * NCic.term list
@@ -76,4 +76,4 @@ val is_out_scope_tag : NCic.meta_attrs -> bool
 val int_of_out_scope_tag : NCic.meta_attrs -> int
 
 val is_flexible:
- #NCic.status -> NCic.context -> subst:NCic.substitution -> NCic.term -> bool
+ #NCicEnvironment.status -> NCic.context -> subst:NCic.substitution -> NCic.term -> bool