id ;-) and lapply patched

[helm.git] / helm / ocaml / tactics / tacticals.ml

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 3c89150adb96f80b1e1721e433eccce810c0d3e4..b72e6e24fae7a678caa5a901b49f1c45bbd09b1d 100644 (file)
--- 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: