X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FvariousTactics.ml;h=fd383cf99dbe76ee977c3c7fa50a52b7aaf73566;hb=refs%2Fheads%2Fmatita-lablgtk3;hp=4652899f038fea8a568b5c624426baac01e0362c;hpb=36842ee77114d2fa896d7ffd2333c07cff22b053;p=helm.git

diff --git a/helm/software/components/tactics/variousTactics.ml b/helm/software/components/tactics/variousTactics.ml
index 4652899f0..fd383cf99 100644
--- a/helm/software/components/tactics/variousTactics.ml
+++ b/helm/software/components/tactics/variousTactics.ml
@@ -38,7 +38,7 @@ let assumption_tac =
   let module R = CicReduction in
   let module S = CicSubstitution in
   let module PT = PrimitiveTactics in
-  let _,metasenv,_subst,_,_, _ = proof in
+  let _,metasenv,_,_,_, _ = proof in
   let _,context,ty = CicUtil.lookup_meta goal metasenv in
   let rec find n = function 
       hd::tl ->