X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_omdoc%2Fcontent2cic.ml;h=d25d7942595f8b20348b1dc37596516f678f3dfd;hb=c43f710f5e23e940114b1623329f650814e783af;hp=1d4dcd1ee885bbaac4c9daa0be69f0f18e4a5220;hpb=a70ce8d5659ab5cd532317e206a30da878ff8a89;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index 1d4dcd1ee..d25d79425 100644
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -167,10 +167,29 @@ let proof2cic deannotate p =
            let  cargs = args2cic premise_env args in
            C.Appl (C.Const(uri,subst)::cargs)
        | _ -> prerr_endline "6"; assert false)
+    else if (conclude.Con.conclude_method = "Case") then
+      (match conclude.Con.conclude_args with
+        Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Premise(prem)::patterns ->
+           C.MutCase
+            (UriManager.uri_of_string uri,
+             int_of_string notype, deannotate ty, 
+             List.assoc prem.Con.premise_xref premise_env,
+             List.map 
+               (function 
+                   Con.ArgProof p -> proof2cic [] p
+		 | _ -> prerr_endline "7a"; assert false) patterns)
+      | Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns ->           C.MutCase
+            (UriManager.uri_of_string uri,
+             int_of_string notype, deannotate ty, deannotate te,
+             List.map 
+               (function 
+                   (Con.ArgProof p) -> proof2cic [] p
+		 | _ -> prerr_endline "7a"; assert false) patterns) 
+      | _ -> (prerr_endline "7"; assert false))
     else if (conclude.Con.conclude_method = "Apply") then
       let cargs = (args2cic premise_env conclude.Con.conclude_args) in
       C.Appl cargs 
-    else (prerr_endline "7"; assert false)
+    else (prerr_endline "8"; assert false)
 
   and args2cic premise_env l =
     List.map (arg2cic premise_env) l