Added universes handling. The PRE_UNIVERSES tag may help ;)

[helm.git] / helm / ocaml / tactics / negationTactics.ml

diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml
index a4b7d9ba844c8868bea0ecc973107b71e67c493d..c8c9785dae9cdfe094c7c7fed6d543fbb9b3aed6 100644 (file)
--- a/helm/ocaml/tactics/negationTactics.ml
+++ b/helm/ocaml/tactics/negationTactics.ml
@@ -29,19 +29,21 @@ let absurd_tac ~term =
   let module C = Cic in
   let module U = UriManager in
   let module P = PrimitiveTactics in
-   let _,metasenv,_,_ = proof in
-    let _,context,ty = CicUtil.lookup_meta goal metasenv in
-     if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
-      then ProofEngineTypes.apply_tactic 
-       (P.apply_tac 
-        ~term:(
-         C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ; 
-                term ; ty])
-       ) 
-       status
-      else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
+  let _,metasenv,_,_ = proof in
+  let _,context,ty = CicUtil.lookup_meta goal metasenv in
+  let ty_term,_ = 
+    CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+    if (ty_term = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
+    then ProofEngineTypes.apply_tactic 
+      (P.apply_tac 
+         ~term:(
+           C.Appl [(C.Const (HelmLibraryObjects.Logic.absurd_URI , [] )) ; 
+                  term ; ty])
+      ) 
+      status
+    else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
  in
-  ProofEngineTypes.mk_tactic (absurd_tac ~term)
+   ProofEngineTypes.mk_tactic (absurd_tac ~term)
 ;;
 
 let contradiction_tac =