Build_proof_goal does not return the metasenv any more.

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

diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli
index 9ef8d2197661b5877e74610441512f4d8571897e..4d48f22aade7a4aa888b99d924963731e918f3ce 100644 (file)
--- a/components/tactics/paramodulation/equality.mli
+++ b/components/tactics/paramodulation/equality.mli
@@ -80,10 +80,9 @@ val string_of_equality : ?env:Utils.environment -> equality -> string
 val string_of_proof_old : ?names:(Cic.name option)list -> old_proof -> string
 val string_of_proof_new : 
   ?names:(Cic.name option)list -> new_proof -> goal_proof -> string
-val build_proof_term_new: new_proof -> Cic.term * Cic.metasenv
+val build_proof_term_new: new_proof -> Cic.term 
 val build_proof_term_old: ?noproof:Cic.term -> old_proof -> Cic.term
-val build_goal_proof: 
-  goal_proof -> (Cic.term * Cic.metasenv) -> Cic.term * Cic.metasenv
+val build_goal_proof: goal_proof -> Cic.term -> Cic.term
 val refl_proof: Cic.term -> Cic.term -> Cic.term 
 (** ensures that metavariables in equality are unique *)
 val fix_metas: int -> equality -> int * equality