split non-logic level of whelp away from metadataQuery to a new module

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

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index a5c7878c7341336a822e39587adcaa5947b9d018..a40dd42b339747cd5720abb515be742761e62aef 100644 (file)
--- 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;