in
let ty_eq,ugraph =
CicTypeChecker.type_of_aux' metasenv context equality
- CicUniv.empty_ugraph in
+ CicUniv.oblivion_ugraph in
let (ty_eq,metasenv',arguments,fresh_meta) =
TermUtil.saturate_term
(ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq 0 in
in
let context_len = List.length context in
let subst,metasenv,u,_,selected_terms_with_context =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+ ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
~conjecture ~pattern in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
let with_what, metasenv, u = with_what context metasenv u in
let status = (uri,metasenv,_subst,pbo,pty, attrs),goal in
let ty_of_with_what,u =
CicTypeChecker.type_of_aux'
- metasenv context with_what CicUniv.empty_ugraph in
+ metasenv context with_what CicUniv.oblivion_ugraph in
let whats =
match selected_terms_with_context with
[] -> raise (ProofEngineTypes.Fail (lazy "Replace: no term selected"))
(lazy "Replace: one of the selected terms is not closed")) in
let ty_of_t_in_context,u = (* TASSI: FIXME *)
CicTypeChecker.type_of_aux' metasenv context t_in_context
- CicUniv.empty_ugraph in
+ CicUniv.oblivion_ugraph in
let b,u = CicReduction.are_convertible ~metasenv context
ty_of_with_what ty_of_t_in_context u in
if b then