X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Flibrary%2FcicRecord.ml;h=85c2ea03676cfef4723a39d8524548a157f48fa0;hb=5dd5b3f6cd990d4d126b44c092e1df7f86c506d4;hp=a251bad87c5b5530b8253f0c8f221e51d5e3b6d9;hpb=2034db684e1d295527afad07a94f2f3b6b4ed7e2;p=helm.git

diff --git a/helm/ocaml/library/cicRecord.ml b/helm/ocaml/library/cicRecord.ml
index a251bad87..85c2ea036 100644
--- 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)