split into two major parts:

[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..4362006447266b1fea7578adca00e4c7e59fa4c4 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 ->
@@ -67,7 +67,7 @@ let whd context =
        )
     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
     | C.Sort _ as t -> t (* l should be empty *)
-    | C.Implicit as t -> t
+    | C.Implicit _ as t -> t
     | C.Cast (te,ty) -> whdaux l te  (*CSC E' GIUSTO BUTTARE IL CAST? *)
     | C.Prod _ as t -> t (* l should be empty *)
     | C.Lambda (name,s,t) as t' ->
@@ -136,7 +136,7 @@ let whd context =
                 eat_first (r,tl)
               in
                whdaux (ts@l) (List.nth pl (j-1))
-          | C.Cast _ | C.Implicit ->
+          | C.Cast _ | C.Implicit _ ->
              raise (Impossible 2) (* we don't trust our whd ;-) *)
           | _ -> if l = [] then t else C.Appl (t::l)
        )
@@ -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 
@@ -287,7 +290,7 @@ let are_convertible =
                 b && aux context ty1 ty2 && aux (tys@context) bo1 bo2)
               fl1 fl2 true
         | (C.Cast _, _) | (_, C.Cast _)
-        | (C.Implicit, _) | (_, C.Implicit) ->
+        | (C.Implicit _, _) | (_, C.Implicit _) ->
            raise (Impossible 3) (* we don't trust our whd ;-) *)
         | (_,_) -> false
     end