X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicReduction.ml;h=8fc58f4c9c27002fe81b8c9930e455e9ba9212f1;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=236f5778e86394317930eababfede4aaedc8fb3e;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 236f5778e..8fc58f4c9 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -61,7 +61,7 @@ module CallByValueByNameForUnwind' : Strategy = struct lazy (fst (reduce ~delta:0 c)), (fun delta -> fst (reduce ~delta c)), lazy (unwind c) - let from_stack ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta + let from_stack ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta let from_stack_list_for_unwind ~unwind:_ l = List.map (fun (_,_,c) -> Lazy.force c) l let from_env ~delta (c0,c,_) = if delta = 0 then Lazy.force c0 else c delta @@ -433,7 +433,6 @@ type machine = int * environment_item list * NCic.term * stack_item list let reduce_machine = R.reduce let from_stack = RS.from_stack -let from_env = RS.from_env let unwind = R.unwind let _ =