This commit patches the environment and the library so that their status is

[helm.git] / matitaB / components / ng_kernel / nCicSubstitution.mli

diff --git a/matitaB/components/ng_kernel/nCicSubstitution.mli b/matitaB/components/ng_kernel/nCicSubstitution.mli
index 9ba2d11fa55bb7e080361647861d35bebff558f1..8db93d0c0493efe352b82577f8096a254051236b 100644 (file)
--- a/matitaB/components/ng_kernel/nCicSubstitution.mli
+++ b/matitaB/components/ng_kernel/nCicSubstitution.mli
@@ -11,14 +11,14 @@
 
 (* $Id$ *)
 
-val lift_from : #NCic.status -> ?no_implicit:bool -> int -> int -> NCic.term -> NCic.term 
+val lift_from : #NCicEnvironment.status -> ?no_implicit:bool -> int -> int -> NCic.term -> NCic.term 
 
 (* lift n t                                                              *)
 (*  lifts [t] of [n]                                                     *)
 (*  [from] default 1, lifts only indexes >= [from]                       *)
 (*  NOTE: the opposite function (delift_rels) is defined in CicMetaSubst *)
 (*  since it needs to restrict the metavariables in case of failure      *)
-val lift : #NCic.status -> ?from:int -> ?no_implicit:bool -> int -> NCic.term -> NCic.term
+val lift : #NCicEnvironment.status -> ?from:int -> ?no_implicit:bool -> int -> NCic.term -> NCic.term
 
 (* subst t1 t2                                                          *)
 (*  substitutes [t1] for [Rel 1] in [t2]                                *)
@@ -26,7 +26,7 @@ val lift : #NCic.status -> ?from:int -> ?no_implicit:bool -> int -> NCic.term ->
 (*  are generated. WARNING: the substitution can diverge when t2 is not *)
 (*  well typed and avoid_beta_redexes is true.                          *)
 val subst : 
-  #NCic.status -> ?avoid_beta_redexes:bool -> ?no_implicit:bool -> 
+  #NCicEnvironment.status -> ?avoid_beta_redexes:bool -> ?no_implicit:bool -> 
   NCic.term -> NCic.term -> NCic.term
 
 (* psubst [avoid] [map_arg] [args] [t]            
@@ -37,7 +37,7 @@ val subst :
  *    the function is ReductionStrategy.from_env_for_unwind when psubst is
  *    used to implement nCicReduction.unwind'                              *)
 val psubst : 
-  #NCic.status -> ?avoid_beta_redexes:bool -> ?no_implicit:bool ->
+  #NCicEnvironment.status -> ?avoid_beta_redexes:bool -> ?no_implicit:bool ->
   ('a -> NCic.term) -> 'a list -> NCic.term -> 
     NCic.term
 
@@ -45,5 +45,5 @@ val psubst :
 (*  returns the term [t] where [Rel i] is substituted with [t_i] lifted by n *)
 (*  [t_i] is lifted as usual when it crosses an abstraction                  *)
 (* subst_meta (n, Irl _) t -> lift n t                                        *)
-val subst_meta : #NCic.status -> NCic.local_context -> NCic.term -> NCic.term
+val subst_meta : #NCicEnvironment.status -> NCic.local_context -> NCic.term -> NCic.term