X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;fp=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=0295daac326659968bb6d8637ad9956583e90afa;hp=0933dbc4b88a573f09a30f1060e3bc14dadc1859;hb=60f8a4de1287ea04ee5722460bdc6ff16a3eb4be;hpb=45bc31f244e06f1eead7c35bc5b812574edf1737

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 0933dbc4b..0295daac3 100644
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -699,8 +699,9 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
       if n<0 then raise NotApplicable
       else 
         let method_name =
-          if uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" then
-            "Exists"
+          if (uri_str = "cic:/Coq/Init/Logic_Type/exT_ind.con" or
+              uri_str = "cic:/Coq/Init/Logic/ex_ind.con") then "Exists"
+          else if uri_str = "cic:/Coq/Init/Logic/and_ind.con" then "AndInd"
           else "ByInduction" in
         let prefix = String.sub uri_str 0 n in
         let ind_str = (prefix ^ ".ind") in