From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 14 Feb 2006 12:18:44 +0000 (+0000)
Subject: fixed syntax
X-Git-Tag: make_still_working~7571
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b78dcf912b4faf5ebcccec28ce3f60475bcdd435;p=helm.git

fixed syntax
---

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 56e98775f..5a638b5f7 100644
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -969,8 +969,8 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
     end
   in
    debug t1 [t2] "PREWHD";
-   let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in
-   let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in
+   let t1' = whd ~delta:true ~subst context t1 in
+   let t2' = whd ~delta:true ~subst context t2 in
     debug t1' [t2'] "POSTWHD";
     aux2 test_equality_only t1' t2' ugraph
  in