X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FnegationTactics.ml;h=fb904bf361df7025b2203cd615133dce4885d0b1;hb=6a0ba36a34474850464f568139fdda5e9d85f315;hp=c973d75f4706d20754266f4c8df2facd686b9ebe;hpb=08a92d276c5477968b02f31097b6ed03185f34eb;p=helm.git

diff --git a/helm/software/components/tactics/negationTactics.ml b/helm/software/components/tactics/negationTactics.ml
index c973d75f4..fb904bf36 100644
--- 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