New reduction strategy (that behaves much better during simplification).

[helm.git] / helm / ocaml / cic_proof_checking / cicReduction.ml

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index 846cdf92b3f2224bcf7bd24a904851519740b56d..56e98775f31caf7276303a091dbeb22612128046 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -746,8 +746,8 @@ module R = Reduction
  ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s
 module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s
 *)
-(*module R = Reduction(CallByValueByNameForUnwind);; *)
-module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
+module R = Reduction(CallByValueByNameForUnwind);;
+(*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*)
 module U = UriManager;;
 
 let whd = R.whd