ocaml 3.09 transition

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

diff --git a/helm/ocaml/cic_proof_checking/cicRecord.ml b/helm/ocaml/cic_proof_checking/cicRecord.ml
index d8dd2dc47b142cc1b7cc9df8469947c1a78080ce..a251bad87c5b5530b8253f0c8f221e51d5e3b6d9 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicRecord.ml
+++ b/helm/ocaml/cic_proof_checking/cicRecord.ml
@@ -40,7 +40,7 @@ let generate_one_proj uri params paramsno fields t i =
        Cic.MutCase (uri,0,outtype, Cic.Rel 1, 
         [mk_lambdas fields (Cic.Rel i)]))))
 
-let projections_of uri =
+let projections_of uri field_names =
  let buri = UriManager.buri_of_uri uri in
  let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
   match obj with
@@ -60,32 +60,32 @@ let projections_of uri =
       let fields =
        let rec aux =
         function
-           Cic.MutInd _
-         | Cic.Appl _ -> []
-         | Cic.Prod (Cic.Name name,s,t) -> (name,s)::aux t
-         | _ -> assert false
+           Cic.MutInd _, []
+         | Cic.Appl _,   [] -> []
+         | Cic.Prod (_,s,t), name::tl -> (name,s)::aux (t,tl)
+         | _,_ -> assert false
        in
-        aux (CicSubstitution.lift 1 ty)
+        aux ((CicSubstitution.lift 1 ty),field_names)
       in
        let rec aux i =
         function
-           Cic.MutInd _
-         | Cic.Appl _ -> []
-         | Cic.Prod (Cic.Name name,s,t) ->
+           Cic.MutInd _, []
+         | Cic.Appl _,   [] -> []
+         | Cic.Prod (_,s,t), name::tl ->
             (match generate_one_proj uri leftparams paramsno fields s i with
-               Some p ->
-                let puri =
-                 UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
-                in
-                 (puri,name,p) ::
-                   aux (i - 1)
-                    (CicSubstitution.subst
-                      (Cic.Appl
-                        (Cic.Const (puri,[]) ::
-                          CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1])
-                      ) t)
-             | None -> assert false)
-         | _ -> assert false
+                Some p ->
+                 let puri =
+                  UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con")
+                 in
+                  (puri,name,p) ::
+                    aux (i - 1)
+                     (CicSubstitution.subst
+                       (Cic.Appl
+                         (Cic.Const (puri,[]) ::
+                           CicUtil.mk_rels paramsno 2 @ [Cic.Rel 1])
+                       ) t, tl)
+              | None -> assert false)
+         | _,_ -> assert false
        in
-        aux (List.length fields) (CicSubstitution.lift 2 ty)
+        aux (List.length fields) (CicSubstitution.lift 2 ty,field_names)
    | _ -> assert false