match get_proof () with
None -> assert false
| Some (uri,metasenv,bo,gty as proof') ->
match get_proof () with
None -> assert false
| Some (uri,metasenv,bo,gty as proof') ->
(* We push the new meta at the end of the list for pretty-printing *)
(* purposes: in this way metas are ordered. *)
let metasenv' = metasenv@[newmeta,context,ty] in
(* We push the new meta at the end of the list for pretty-printing *)
(* purposes: in this way metas are ordered. *)
let metasenv' = metasenv@[newmeta,context,ty] in
(*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
let bo' =
ProofEngineReduction.replace (==) [term] [C.Meta (newmeta,irl)] bo
(*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
let bo' =
ProofEngineReduction.replace (==) [term] [C.Meta (newmeta,irl)] bo