X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicReduction.mli;h=713edd1705050d14fe6ee2d1fee270a71f7fd713;hb=8dbc4dcef7328f3ac84f847255e9be8d47c1de6d;hp=ba32fe15dd18f2cb38c6af0dc055fae94d72bbe5;hpb=bfaa39fb1d8cd4abd07c23a61c69630f9da33157;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli index ba32fe15d..713edd170 100644 --- a/helm/software/components/ng_kernel/nCicReduction.mli +++ b/helm/software/components/ng_kernel/nCicReduction.mli @@ -13,6 +13,8 @@ exception AssertFailure of string Lazy.t;; +val debug: bool ref + val whd : ?delta:int -> subst:NCic.substitution -> NCic.context -> NCic.term -> @@ -41,7 +43,7 @@ type machine = int * environment_item list * NCic.term * stack_item list val reduce_machine : delta:int -> ?subst:NCic.substitution -> NCic.context -> machine -> machine * bool -val from_stack : stack_item -> machine +val from_stack : delta:int -> stack_item -> machine val unwind : machine -> NCic.term val split_prods: