X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_kernel%2FnCicReduction.mli;h=afe09ddae53cff552cf3116a754428fdbedbc951;hb=9aa2722ff4aa7868ffd14e5a820cd6dc79e2c8a6;hp=f53cb5dc830631272b7529a6e07c84db5a3413f0;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/ng_kernel/nCicReduction.mli b/matitaB/components/ng_kernel/nCicReduction.mli
index f53cb5dc8..afe09ddae 100644
--- a/matitaB/components/ng_kernel/nCicReduction.mli
+++ b/matitaB/components/ng_kernel/nCicReduction.mli
@@ -16,15 +16,15 @@ exception AssertFailure of string Lazy.t;;
 val debug: bool ref
 
 val whd : 
-  #NCic.status -> ?delta:int -> subst:NCic.substitution -> 
+  #NCicEnvironment.status -> ?delta:int -> subst:NCic.substitution -> 
   NCic.context -> NCic.term -> NCic.term
 
 val set_get_relevance : 
-  (NCic.status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
+  (NCicEnvironment.status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
    NCic.context -> NCic.term -> NCic.term list -> bool list) -> unit
 
 val are_convertible :
-  #NCic.status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
+  #NCicEnvironment.status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
   NCic.context -> NCic.term -> NCic.term -> bool
 
 
@@ -32,7 +32,7 @@ val are_convertible :
    delta reduction; if provided, ~upto is the maximum number of beta redexes
    reduced *)
 val head_beta_reduce: 
- #NCic.status -> ?delta:int -> ?upto:int -> ?subst:NCic.substitution ->
+  #NCicEnvironment.status -> ?delta:int -> ?upto:int -> ?subst:NCic.substitution ->
   NCic.term -> NCic.term
 
 type stack_item
@@ -41,17 +41,17 @@ type environment_item
 type machine = int * environment_item list * NCic.term * stack_item list
 
 val reduce_machine : 
- #NCic.status -> delta:int -> ?subst:NCic.substitution -> NCic.context ->
+ #NCicEnvironment.status -> delta:int -> ?subst:NCic.substitution -> NCic.context ->
   machine -> machine * bool
 val from_stack : delta:int -> stack_item -> machine
 val from_env : delta:int -> environment_item -> machine
-val unwind : #NCic.status -> machine -> NCic.term
+val unwind : #NCicEnvironment.status -> machine -> NCic.term
 
 val split_prods:
- #NCic.status -> subst:NCic.substitution -> NCic.context -> int -> NCic.term ->
+ #NCicEnvironment.status -> subst:NCic.substitution -> NCic.context -> int -> NCic.term ->
   NCic.context * NCic.term
 
 (* to be used outside the kernel *)
 val alpha_eq:
- #NCic.status -> NCic.metasenv -> NCic.substitution -> NCic.context ->
+ #NCicEnvironment.status -> NCic.metasenv -> NCic.substitution -> NCic.context ->
   NCic.term -> NCic.term -> bool