let cargs = args2cic premise_env args in
C.Appl (C.Const(uri,subst)::cargs)
| _ -> prerr_endline "6"; assert false)
+ else if (conclude.Con.conclude_method = "Case") then
+ (match conclude.Con.conclude_args with
+ Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Premise(prem)::patterns ->
+ C.MutCase
+ (UriManager.uri_of_string uri,
+ int_of_string notype, deannotate ty,
+ List.assoc prem.Con.premise_xref premise_env,
+ List.map
+ (function
+ Con.ArgProof p -> proof2cic [] p
+ | _ -> prerr_endline "7a"; assert false) patterns)
+ | Con.Aux(uri)::Con.Aux(notype)::Con.Term(ty)::Con.Term(te)::patterns -> C.MutCase
+ (UriManager.uri_of_string uri,
+ int_of_string notype, deannotate ty, deannotate te,
+ List.map
+ (function
+ (Con.ArgProof p) -> proof2cic [] p
+ | _ -> prerr_endline "7a"; assert false) patterns)
+ | _ -> (prerr_endline "7"; assert false))
else if (conclude.Con.conclude_method = "Apply") then
let cargs = (args2cic premise_env conclude.Con.conclude_args) in
C.Appl cargs
- else (prerr_endline "7"; assert false)
+ else (prerr_endline "8"; assert false)
and args2cic premise_env l =
List.map (arg2cic premise_env) l
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 ->