X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicReduction.ml;h=316b39dabb8ee3403f9e1bd55f1f7596d7dc1cf0;hb=761aef3c864626e17004b9785c39def7053271e0;hp=cc4d99e05473c1d2aeecef9b5103f40b0c803987;hpb=0bd584a839bae570f44c4a5f8a06cdbc55fe0726;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index cc4d99e05..316b39dab 100644
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -365,4 +365,13 @@ let rec head_beta_reduce ?(delta=max_int) ?(upto=(-1)) t l =
 
 let head_beta_reduce ?delta ?upto t = head_beta_reduce ?delta ?upto t [];;
 
+type stack_item = RS.stack_term
+type environment_item = RS.env_term
+
+type machine = int * environment_item list * NCic.term * stack_item list
+
+let reduce_machine = R.reduce
+let from_stack = RS.from_stack
+let unwind = R.unwind
+
 (* vim:set foldmethod=marker: *)