X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FfwdSimplTactic.ml;h=0bae64f6c6fb7bb1e22a1ac84d4400cc4e0ae20a;hb=6bbeb650abc3a94e76d683aa47b2e46254d495d1;hp=a5c7878c7341336a822e39587adcaa5947b9d018;hpb=dbe5d5ee749b3d5d36c91f96b73d7554967fc8cd;p=helm.git

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index a5c7878c7..0bae64f6c 100644
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -23,6 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
 
 module PEH = ProofEngineHelpers 
 module U  = CicUniv
@@ -132,7 +133,7 @@ let fwd_simpl_tac
       let _, metasenv, _, _ = proof in
       let _, context, ty = CicUtil.lookup_meta goal metasenv in
       let index, major = PEH.lookup_type metasenv context hyp in 
-      match MetadataQuery.fwd_simpl ~dbd major with
+      match FwdQueries.fwd_simpl ~dbd major with
          | []       -> error fail_msg2
          | uri :: _ -> 
 	    Printf.eprintf "fwd: %s\n" (UriManager.string_of_uri uri); flush stderr;