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=107e3b81911ca470d0422b190811e692947afa52;hpb=fc7466b8428ea409d97c0dfa347de9f4f51cb582;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/inference.mli b/helm/software/components/tactics/paramodulation/inference.mli
index 107e3b819..b08054ca4 100644
--- a/helm/software/components/tactics/paramodulation/inference.mli
+++ b/helm/software/components/tactics/paramodulation/inference.mli
@@ -142,4 +142,5 @@ val metas_of_proof: proof -> int list
 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