Defs in context may now have an optional type (when unknown).

[helm.git] / helm / ocaml / cic_omdoc / content2cic.ml

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index 1d4dcd1ee885bbaac4c9daa0be69f0f18e4a5220..ed62e254cc0b6a499560a48c1c63838273706504 100644 (file)
--- 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
@@ -188,6 +207,11 @@ let proof2cic deannotate p =
                with Not_found -> 
                   prerr_endline ("Not_found in arg2cic: premise " ^ (match prem.Con.premise_binder with None -> "previous" | Some p -> p) ^ ", xref=" ^ prem.Con.premise_xref);
                   raise Not_found))
+      | Con.Lemma lemma -> 
+          MQueryMisc.term_of_cic_textual_parser_uri 
+           (MQueryMisc.cic_textual_parser_uri_of_string
+            (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
+              lemma.Con.lemma_uri))
       | Con.Term t -> 
           deannotate t
       | Con.ArgProof p ->
@@ -214,22 +238,23 @@ let cobj2obj deannotate (id,params,metasenv,obj) =
                let canonical_context' =
                 List.map
                  (function
-                     _,None -> None
-                   | _,Some (`Declaration d) 
-                   | _,Some (`Hypothesis d) ->
+                     None -> None
+                   | Some (`Declaration d) 
+                   | Some (`Hypothesis d) ->
                      (match d with
                         {K.dec_name = Some n ; K.dec_type = t} ->
                           Some (Cic.Name n, Cic.Decl (deannotate t))
                       | _ -> assert false)
-                   | _,Some (`Definition d) ->
+                   | Some (`Definition d) ->
                       (match d with
                           {K.def_name = Some n ; K.def_term = t} ->
-                            Some (Cic.Name n, Cic.Def (deannotate t))
+                            Some (Cic.Name n, Cic.Def ((deannotate t),None))
                         | _ -> assert false)
-                   | _,Some (`Proof d) ->
+                   | Some (`Proof d) ->
                       (match d with
                           {K.proof_name = Some n } ->
-                            Some (Cic.Name n, Cic.Def (proof2cic deannotate d))
+                            Some (Cic.Name n,
+                              Cic.Def ((proof2cic deannotate d),None))
                         | _ -> assert false)
                  ) canonical_context
                in