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

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index a5c7878c7..a40dd42b3 100644
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -132,7 +132,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;