X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicSubstitution.mli;h=9ba2d11fa55bb7e080361647861d35bebff558f1;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=7e27a5d4ceab9cf82b05c9d4259d116a4150e187;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_kernel/nCicSubstitution.mli b/matita/components/ng_kernel/nCicSubstitution.mli
index 7e27a5d4c..9ba2d11fa 100644
--- a/matita/components/ng_kernel/nCicSubstitution.mli
+++ b/matita/components/ng_kernel/nCicSubstitution.mli
@@ -11,20 +11,14 @@
 
 (* $Id$ *)
 
-val set_ppterm : (context:NCic.context -> 
-  subst:NCic.substitution -> 
-  metasenv:NCic.metasenv ->
-  ?inside_fix:bool ->
-   NCic.term -> string) -> unit
-
-val lift_from : ?no_implicit:bool -> int -> int -> NCic.term -> NCic.term 
+val lift_from : #NCic.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 : ?from:int -> ?no_implicit:bool -> int -> NCic.term -> NCic.term
+val lift : #NCic.status -> ?from:int -> ?no_implicit:bool -> int -> NCic.term -> NCic.term
 
 (* subst t1 t2                                                          *)
 (*  substitutes [t1] for [Rel 1] in [t2]                                *)
@@ -32,7 +26,7 @@ val lift : ?from:int -> ?no_implicit:bool -> int -> NCic.term -> NCic.term
 (*  are generated. WARNING: the substitution can diverge when t2 is not *)
 (*  well typed and avoid_beta_redexes is true.                          *)
 val subst : 
-  ?avoid_beta_redexes:bool -> ?no_implicit:bool -> 
+  #NCic.status -> ?avoid_beta_redexes:bool -> ?no_implicit:bool -> 
   NCic.term -> NCic.term -> NCic.term
 
 (* psubst [avoid] [map_arg] [args] [t]            
@@ -43,7 +37,7 @@ val subst :
  *    the function is ReductionStrategy.from_env_for_unwind when psubst is
  *    used to implement nCicReduction.unwind'                              *)
 val psubst : 
-  ?avoid_beta_redexes:bool -> ?no_implicit:bool ->
+  #NCic.status -> ?avoid_beta_redexes:bool -> ?no_implicit:bool ->
   ('a -> NCic.term) -> 'a list -> NCic.term -> 
     NCic.term
 
@@ -51,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.local_context -> NCic.term -> NCic.term
+val subst_meta : #NCic.status -> NCic.local_context -> NCic.term -> NCic.term