]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/fwdSimplTactic.ml
Added $Id$ to every .ml file.
[helm.git] / helm / ocaml / tactics / fwdSimplTactic.ml
index a5c7878c7341336a822e39587adcaa5947b9d018..0bae64f6c6fb7bb1e22a1ac84d4400cc4e0ae20a 100644 (file)
@@ -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;