parameter sintax added to axiom statement

[helm.git] / helm / software / components / tactics / negationTactics.ml

diff --git a/helm/software/components/tactics/negationTactics.ml b/helm/software/components/tactics/negationTactics.ml
index c973d75f4706d20754266f4c8df2facd686b9ebe..287ec4dfe4ae2e68271865b607e2456afb282200 100644 (file)
--- a/helm/software/components/tactics/negationTactics.ml
+++ b/helm/software/components/tactics/negationTactics.ml
@@ -31,7 +31,7 @@ let absurd_tac ~term =
   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
@@ -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