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
with Not_found ->
prerr_endline ("Not_found in arg2cic: premise " ^ (match prem.Con.premise_binder with None -> "previous" | Some p -> p) ^ ", xref=" ^ prem.Con.premise_xref);
raise Not_found))
- | Con.Lemma lemma ->
- MQueryMisc.term_of_cic_textual_parser_uri
- (MQueryMisc.cic_textual_parser_uri_of_string
- (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
- lemma.Con.lemma_uri))
- | Con.Term t ->
- deannotate t
- | Con.ArgProof p ->
- proof2cic [] p (* empty! *)
+ | Con.Lemma lemma -> CicUtil.term_of_uri lemma.Con.lemma_uri
+ | Con.Term t -> deannotate t
+ | Con.ArgProof p -> proof2cic [] p (* empty! *)
| Con.ArgMethod s -> raise TO_DO
in proof2cic [] p
(match metasenv with
None ->
Cic.Constant
- (id, Some (proof2cic deannotate bo), deannotate ty, params)
+ (id, Some (proof2cic deannotate bo), deannotate ty, params, [])
| Some metasenv' ->
let metasenv'' =
List.map
) metasenv'
in
Cic.CurrentProof
- (id, metasenv'', proof2cic deannotate bo, deannotate ty, params))
+ (id, metasenv'', proof2cic deannotate bo, deannotate ty, params,
+ []))
| _ -> raise ToDo
;;