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