Added method "FalseInd".

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 335296effff7b374a7a4379f3d56a86828bcfff6..e767b0f1980868e09c4563ff65b0fece071419f0 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -671,6 +671,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
           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 if uri_str = "cic:/Coq/Init/Logic/False_ind.con" then "FalseInd"
           else "ByInduction" in
         let prefix = String.sub uri_str 0 n in
         let ind_str = (prefix ^ ".ind") in 
@@ -687,9 +688,6 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
           let p,a = split (n-1) (List.tl l) in
           ((List.hd l::p),a) in
         let params_and_IP,tail_args = split (noparams+1) args in
-        if method_name = "Exists" then
-          (prerr_endline ("+++++args++++:" ^ string_of_int (List.length args));
-           prerr_endline ("+++++tail++++:" ^ string_of_int (List.length tail_args)));
         let constructors = 
             (match inductive_types with
               [(_,_,_,l)] -> l