X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FtacticChaser.ml;h=f7ea9d9e3bbff3c9dd09c105a5631e7dc7e6b758;hb=HEAD;hp=cb700f776c5debbdfb6bbd716339b2b472ddd4a3;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/tactics/tacticChaser.ml b/helm/software/components/tactics/tacticChaser.ml
index cb700f776..f7ea9d9e3 100644
--- a/helm/software/components/tactics/tacticChaser.ml
+++ b/helm/software/components/tactics/tacticChaser.ml
@@ -237,7 +237,7 @@ let  searchTheorems mqi_handle (proof,goal) =
    prerr_endline "PRIMA DELLA PRIMA TYPE OF " ;
 *)
    let ty_sort1,u = (*TASSI: FIXME *)
-     CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph in
+     CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.oblivion_ugraph in
 (*
    prerr_endline (Printf.sprintf "PRIMA DELLA SECONDA TYPE OF %s \n### %s @@@%s " (CicMetaSubst.ppmetasenv metasenv []) (CicMetaSubst.ppcontext [] ey2) (CicMetaSubst.ppterm [] ty2));
 *)