Big commit to let Ferruccio try the merge_coercion patch.

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

diff --git a/helm/ocaml/library/cicRecord.ml b/helm/ocaml/library/cicRecord.ml
index a251bad87c5b5530b8253f0c8f221e51d5e3b6d9..85c2ea03676cfef4723a39d8524548a157f48fa0 100644 (file)
--- a/helm/ocaml/library/cicRecord.ml
+++ b/helm/ocaml/library/cicRecord.ml
@@ -34,7 +34,6 @@ let generate_one_proj uri params paramsno fields t i =
     Cic.Lambda (Cic.Name name,ty,acc)) l start in
  let recty = rec_ty uri paramsno in
  let outtype = Cic.Lambda (Cic.Name "w'", CicSubstitution.lift 1 recty, t) in
-  Some
    (mk_lambdas params
      (Cic.Lambda (Cic.Name "w", recty,
        Cic.MutCase (uri,0,outtype, Cic.Rel 1, 
@@ -72,19 +71,15 @@ let projections_of uri field_names =
            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, tl)
-              | None -> assert false)
+            let p = generate_one_proj uri leftparams paramsno fields s i in
+            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)
          | _,_ -> assert false
        in
         aux (List.length fields) (CicSubstitution.lift 2 ty,field_names)