let module C = Cic in
let module U = UriManager in
let module P = PrimitiveTactics in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
let absurd_URI =
match LibraryObjects.absurd_URI () with
| None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"absurd\" theorem first. Please use the \"default\" command"))
in
let ty_term,_ =
- CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ CicTypeChecker.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
if (ty_term = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
then ProofEngineTypes.apply_tactic
(P.apply_tac