...

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

diff --git a/helm/software/components/tactics/variousTactics.ml b/helm/software/components/tactics/variousTactics.ml
index 4652899f038fea8a568b5c624426baac01e0362c..fd383cf99dbe76ee977c3c7fa50a52b7aaf73566 100644 (file)
--- 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 ->