X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionNaif.ml;h=5dce7c68da4eec64a6b33f09c4cdf365cb99c9e4;hb=970ba0021a992efe25ec374875dc127ff236cc74;hp=581c5918f4c78c301c1ba65009cc48aa2fc222da;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index 581c5918f..5dce7c68d 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -53,8 +53,8 @@ let whd context =
       C.Rel n as t ->
        (match List.nth context (n-1) with
            Some (_, C.Decl _) -> if l = [] then t else C.Appl (t::l)
-         | Some (_, C.Def bo) -> whdaux l (S.lift n bo)
-	 | None -> raise RelToHiddenHypothesis
+         | Some (_, C.Def (bo,_)) -> whdaux l (S.lift n bo)
+	  | None -> raise RelToHiddenHypothesis
        )
     | C.Var (uri,exp_named_subst) as t ->
        (match CicEnvironment.get_cooked_obj ~trust:false uri with
@@ -217,11 +217,14 @@ let are_convertible =
               ) true l1 l2
         | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
-           aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+           aux context s1 s2 &&
+            aux ((Some (name1, (C.Decl s1)))::context) t1 t2
         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
-           aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+           aux context s1 s2 &&
+            aux ((Some (name1, (C.Decl s1)))::context) t1 t2
         | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
-           aux context s1 s2 && aux ((Some (name1, (C.Def s1)))::context) t1 t2
+           aux context s1 s2 &&
+            aux ((Some (name1, (C.Def (s1,None))))::context) t1 t2
         | (C.Appl l1, C.Appl l2) ->
            (try
              List.fold_right2 (fun  x y b -> aux context x y && b) l1 l2 true