X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FnegationTactics.ml;h=287ec4dfe4ae2e68271865b607e2456afb282200;hb=2e2648a9ed26d9b813de8e6a10e2776162565f09;hp=fb904bf361df7025b2203cd615133dce4885d0b1;hpb=5cd2efd21063b304c30a9486a562bdff7852957b;p=helm.git

diff --git a/helm/software/components/tactics/negationTactics.ml b/helm/software/components/tactics/negationTactics.ml
index fb904bf36..287ec4dfe 100644
--- a/helm/software/components/tactics/negationTactics.ml
+++ b/helm/software/components/tactics/negationTactics.ml
@@ -39,7 +39,7 @@ let absurd_tac ~term =
     | 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