"Performance bug" fixed: I removed a whd in the does_not_occur function.

[helm.git] / helm / software / components / cic_proof_checking / cicReduction.ml

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 56e98775f31caf7276303a091dbeb22612128046..18259a00441873ea85ea755e3a06e891de291872 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -357,7 +357,7 @@ module Reduction(RS : Strategy) =
            let d =
             try
              Some (RS.from_env_for_unwind ~unwind (List.nth e (n-m-1)))
-            with _ -> None
+            with Failure _ -> None
            in
             (match d with 
                 Some t' ->
@@ -639,7 +639,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
         in
          (match decofix (reduce (k,e,ens,term,[])) with
              (k', e', ens', C.MutConstruct (_,_,j,_), []) ->
-              reduce (k, e, ens, (List.nth pl (j-1)), [])
+              reduce (k, e, ens, (List.nth pl (j-1)), s)
            | (k', e', ens', C.MutConstruct (_,_,j,_), s') ->
               let (arity, r) =
                 let o,_ = 
@@ -682,7 +682,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
           try
            Some (RS.from_stack (List.nth s recindex))
           with
-           _ -> None
+           Failure _ -> None
          in
           (match recparam with
               Some recparam ->