From 02e01a974c255e070e5e2638f7a09175e1618a43 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 29 Jul 2003 14:59:08 +0000 Subject: [PATCH] Added method "FalseInd". --- helm/ocaml/cic_omdoc/cic2content.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) 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 -- 2.39.2