From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 29 Jul 2003 14:59:08 +0000 (+0000)
Subject: Added method "FalseInd".
X-Git-Tag: LucaOK~16
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=02e01a974c255e070e5e2638f7a09175e1618a43;p=helm.git

Added method "FalseInd".
---

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 335296eff..e767b0f19 100644
--- 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