added eta expansion to avoid universe inconsistency.

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

diff --git a/components/tactics/negationTactics.ml b/components/tactics/negationTactics.ml
index c973d75f4706d20754266f4c8df2facd686b9ebe..e77fdf4de30269800c4ccf36b084ee2792fcdb30 100644 (file)
--- a/components/tactics/negationTactics.ml
+++ b/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,_,_, _ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
   let absurd_URI =
    match LibraryObjects.absurd_URI () with