X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fequality.mli;h=2d7e48e5cb13dd18ba66d6f0f7543622630b26e3;hb=d72ed76ff623127f76d91aaff98bd2c109bfcd75;hp=9ef8d2197661b5877e74610441512f4d8571897e;hpb=a060ed37101ce0e97bc26af8d49ce2491471c60c;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli
index 9ef8d2197..2d7e48e5c 100644
--- a/helm/software/components/tactics/paramodulation/equality.mli
+++ b/helm/software/components/tactics/paramodulation/equality.mli
@@ -45,7 +45,8 @@ and old_proof =
   | SubProof of Cic.term * int * old_proof
 
 and goal_proof = (Utils.pos * int * substitution * Cic.term) list
-	
+
+val pp_proof: (Cic.name option) list -> goal_proof -> string
 
 val empty_subst : substitution
 val apply_subst : substitution -> Cic.term -> Cic.term
@@ -69,6 +70,10 @@ val mk_equality :
   (Cic.term * Cic.term * Cic.term * Utils.comparison) *
   Cic.metasenv -> 
     equality
+
+val mk_tmp_equality :
+  int * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv -> 
+    equality
     
 val open_equality :
   equality ->
@@ -80,10 +85,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