added tentative elim

[helm.git] / helm / software / components / ng_kernel / nCicReduction.ml

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 0393fbcdd7f5927d06cb44c0903f8d91f352ec3d..2b1d4119b51b4ec6d7b9206d289a704d2d4bc383 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -400,8 +400,11 @@ let from_stack = RS.from_stack
 let unwind = R.unwind
 
 let _ = 
-  NCicUtils.set_head_beta_reduce (fun ~upto t -> head_beta_reduce ~upto t)
+  NCicUtils.set_head_beta_reduce (fun ~upto t -> head_beta_reduce ~upto t);
+  NCicPp.set_head_beta_reduce (fun ~upto t -> head_beta_reduce ~upto t);
 ;;
 
 
+
+
 (* vim:set foldmethod=marker: *)