X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Finference.mli;h=b08054ca4f2c90c72dc97ade2d53e493b8ed0260;hb=1589ec067f5f18594dfcab61431adbe095db1bd1;hp=dd2d4caa17840e1aaf2fbf3b5ac626fcd6897b35;hpb=fd65a0a393bfb43d88ff936f40f045511e900e26;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/inference.mli b/helm/software/components/tactics/paramodulation/inference.mli
index dd2d4caa1..b08054ca4 100644
--- a/helm/software/components/tactics/paramodulation/inference.mli
+++ b/helm/software/components/tactics/paramodulation/inference.mli
@@ -25,6 +25,9 @@
 
 val metas_of_proof_time : float ref
 
+(* type substitution = Cic.substitution *)
+type substitution = (int * Cic.term) list 
+
 type equality =
     int *                (* weight *)
     proof *              (* proof *)
@@ -36,9 +39,9 @@ type equality =
 
 and proof =
   | NoProof   (* no proof *)
-  | BasicProof of Cic.term (* already a proof of a goal *)
+  | BasicProof of substitution * Cic.term (* already a proof of a goal *)
   | ProofBlock of (* proof of a rewrite step *)
-      Cic.substitution * UriManager.uri * (* eq_ind or eq_ind_r *)
+      substitution * UriManager.uri * (* eq_ind or eq_ind_r *)
         (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
   | ProofGoalBlock of proof * proof
       (* proof of the new meta, proof of the goal from which this comes *)
@@ -53,7 +56,7 @@ val build_proof_term: ?noproof:Cic.term -> proof -> Cic.term
 
 val string_of_proof: proof -> string
 
-val filter : Cic.substitution -> Cic.metasenv -> Cic.metasenv
+val filter : substitution -> Cic.metasenv -> Cic.metasenv
 
 exception MatchingFailure
 
@@ -61,7 +64,7 @@ exception MatchingFailure
 val matching:
   Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-  Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+  substitution * Cic.metasenv * CicUniv.universe_graph
 
 (**
    special unification that checks if the two terms are "simple", and in
@@ -70,7 +73,7 @@ val matching:
 val unification:
   Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-  Cic.substitution * Cic.metasenv * CicUniv.universe_graph
+  substitution * Cic.metasenv * CicUniv.universe_graph
 
     
 (**
@@ -131,8 +134,13 @@ val is_identity: environment -> equality -> bool
 
 val string_of_equality: ?env:environment -> equality -> string
 
+
 val metas_of_term: Cic.term -> int list
 val metas_of_proof: proof -> int list
 
 (** ensures that metavariables in equality are unique *)
 val fix_metas: int -> equality -> int * equality
+
+val apply_subst: substitution -> Cic.term -> Cic.term
+val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv
+val ppsubst: substitution -> string