From 0ba7fd95ab7e707e3d4242479d957badcc6009c1 Mon Sep 17 00:00:00 2001
From: Alberto Griggio <griggio@fbk.eu>
Date: Fri, 13 May 2005 09:15:33 +0000
Subject: [PATCH] exported new_metasenv_for_apply, needed by the paramodulation
 stuff...

---
 helm/ocaml/tactics/primitiveTactics.mli | 5 +++++
 1 file changed, 5 insertions(+)

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 ->
-- 
2.39.2