let is_big_general countterm p =
let maxsize = Cexpr2pres.maxsize in
- let module Con = Cic2content in
+ let module Con = Content in
let rec countp current_size p =
if current_size > maxsize then current_size
else
;;
let make_args_for_apply term2pres args =
- let module Con = Cic2content in
+ let module Con = Content in
let module P = Mpresentation in
let rec make_arg_for_apply is_first arg row =
(match arg with
| _ -> assert false;;
let rec justification term2pres p =
- let module Con = Cic2content in
+ let module Con = Content in
let module P = Mpresentation in
if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or
((p.Con.proof_context = []) &
and proof2pres term2pres p =
let rec proof2pres p =
- let module Con = Cic2content in
+ let module Con = Content in
let module P = Mpresentation in
let indent =
let is_decl e =
and ce2pres =
let module P = Mpresentation in
- let module Con = Cic2content in
+ let module Con = Content in
function
`Declaration d ->
(match d.Con.dec_name with
[P.Mtd ([], conclude_aux conclude)])
and conclude_aux conclude =
- let module Con = Cic2content in
+ let module Con = Content in
let module P = Mpresentation in
if conclude.Con.conclude_method = "TD_Conversion" then
let expected =
and arg2pres =
let module P = Mpresentation in
- let module Con = Cic2content in
+ let module Con = Content in
function
Con.Aux n ->
P.Mtext ([],"aux " ^ string_of_int n)
and byinduction conclude =
let module P = Mpresentation in
- let module Con = Cic2content in
+ let module Con = Content in
let proof_conclusion =
(match conclude.Con.conclude_conclusion with
None -> P.Mtext([],"No conclusion???")
and make_case =
let module P = Mpresentation in
- let module Con = Cic2content in
+ let module Con = Content in
function
Con.ArgProof p ->
let name =
exception ToDo;;
let content2pres term2pres (id,params,metasenv,obj) =
- let module Con = Cic2content in
+ let module Con = Content in
let module P = Mpresentation in
match obj with
`Def (Con.Const,thesis,`Proof p) ->