HUGE COMMIT:

[helm.git] / matita / components / ng_kernel / nCicReduction.mli

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