Lemma generated wrong URIs (again). Fixed.

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index b1151c792400ea6f4986a82040b03eb65b965d5b..644f55920bd76e72ebb9529ee62ba54a9e0b658e 100644 (file)
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -177,14 +177,14 @@ let proof2cic deannotate p =
              List.map 
                (function 
                    Con.ArgProof p -> proof2cic [] p
-                | _ -> prerr_endline "7a"; assert false) patterns)
+                 | _ -> 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 "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
@@ -208,8 +208,10 @@ let proof2cic deannotate p =
                   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 lemma.Con.lemma_uri)
+          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 ->