Defs in context may now have an optional type (when unknown).

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

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index 987f4b6edbd8bc932207aeee2f493b2ea8135986..5dce7c68da4eec64a6b33f09c4cdf365cb99c9e4 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -53,7 +53,7 @@ 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)
+         | Some (_, C.Def (bo,_)) -> whdaux l (S.lift n bo)
          | None -> raise RelToHiddenHypothesis
        )
     | C.Var (uri,exp_named_subst) as t ->
@@ -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