More robust handling of Control-C.

[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 5a638b5f763dff99df786eda8413678bfa3c1c9e..046ab908ab1b66a20f2291ddb5837ba1b3ae9900 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -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,_ = 
@@ -969,8 +969,8 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
     end
   in
    debug t1 [t2] "PREWHD";
-   let t1' = whd ~delta:true ~subst context t1 in
-   let t2' = whd ~delta:true ~subst context t2 in
+   let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
+   let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
     debug t1' [t2'] "POSTWHD";
     aux2 test_equality_only t1' t2' ugraph
  in