X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcontent2cic.ml;h=65ea0d3069efc56f460ac632aefaf4590732531a;hb=e1d3db51fb0d63c882c0a40d9b91bc28ab05747e;hp=ed62e254cc0b6a499560a48c1c63838273706504;hpb=a335fa89b0340ba3fb5d60566075ca83b5bda5d1;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index ed62e254c..65ea0d306 100644
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -149,7 +149,10 @@ let proof2cic deannotate p =
       (match conclude.Con.conclude_args with
          [Con.ArgProof p] -> proof2cic [] p (* empty! *)
        | _ -> prerr_endline "4"; assert false)
-    else if (conclude.Con.conclude_method = "ByInduction") then
+    else if (conclude.Con.conclude_method = "ByInduction" ||
+             conclude.Con.conclude_method = "AndInd" ||
+             conclude.Con.conclude_method = "Exists" ||
+             conclude.Con.conclude_method = "FalseInd") then
       (match (List.tl conclude.Con.conclude_args) with
          Con.Term (C.AAppl 
             id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args ->