From: Alberto Griggio <griggio@fbk.eu>
Date: Fri, 13 May 2005 09:15:33 +0000 (+0000)
Subject: exported new_metasenv_for_apply, needed by the paramodulation stuff...
X-Git-Tag: single_binding~77
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0ba7fd95ab7e707e3d4242479d957badcc6009c1;p=helm.git

exported new_metasenv_for_apply, needed by the paramodulation stuff...
---

diff --git a/helm/ocaml/tactics/primitiveTactics.mli b/helm/ocaml/tactics/primitiveTactics.mli
index 653894637..a6e506432 100644
--- a/helm/ocaml/tactics/primitiveTactics.mli
+++ b/helm/ocaml/tactics/primitiveTactics.mli
@@ -23,6 +23,11 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* ALB needed for paramodulation... *)
+val new_metasenv_for_apply:
+  int -> ProofEngineTypes.proof -> Cic.context -> Cic.term ->
+  Cic.term * Cic.metasenv * Cic.term list * int
+
 (* not a real tactic *)
 val apply_tac_verbose :
   term:Cic.term ->