- patch to consider the symbols of the goal when computing the weight of an

[helm.git] / components / tactics / paramodulation / utils.mli

diff --git a/components/tactics/paramodulation/utils.mli b/components/tactics/paramodulation/utils.mli
index c64eacfd61f3c3364df483305e51624d04e96aab..d761045b85a75c18eb27d36e66cff82c558f518e 100644 (file)
--- a/components/tactics/paramodulation/utils.mli
+++ b/components/tactics/paramodulation/utils.mli
@@ -63,6 +63,7 @@ val names_of_context: Cic.context -> (Cic.name option) list
 module TermMap: Map.S with type key = Cic.term
 
 val symbols_of_term: Cic.term -> int TermMap.t
+val set_goal_symbols: Cic.term -> unit
 
 val lpo: Cic.term -> Cic.term -> comparison