X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ftacticals.ml;fp=helm%2Focaml%2Ftactics%2Ftacticals.ml;h=b72e6e24fae7a678caa5a901b49f1c45bbd09b1d;hb=e9e3089b886e88a07267743cae79d6a9cabdd3c3;hp=3c89150adb96f80b1e1721e433eccce810c0d3e4;hpb=d4c4624f1d083e4ebcba6c276e6caa1972b627dc;p=helm.git

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 3c89150ad..b72e6e24f 100644
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -44,9 +44,12 @@ let warn s =
   (* not a tactical, but it's used only here (?) *)
 
 let id_tac = 
- let tac (proof,goal) = (proof,[goal])
+ let id_tac (proof,goal) = 
+  let _, metasenv, _, _ = proof in
+  let _, _, _ = CicUtil.lookup_meta goal metasenv in
+  (proof,[goal])
  in 
-  mk_tactic tac
+  mk_tactic id_tac
 
   (**
     naive implementation of ORELSE tactical, try a sequence of tactics in turn: