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

diff --git a/helm/ocaml/library/cicRecord.ml b/helm/ocaml/library/cicRecord.ml
index a251bad87..775292ccb 100644
--- a/helm/ocaml/library/cicRecord.ml
+++ b/helm/ocaml/library/cicRecord.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 let rec_ty uri leftno  = 
   let rec_ty = Cic.MutInd (uri,0,[]) in
   if leftno = 0 then rec_ty else
@@ -34,7 +36,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 +73,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)