(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 ->
+ Con.Term (C.AAppl (
+ id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))::args ->
let subst =
List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in
let cargs = args2cic premise_env args in