fix for distro

[helm.git] / helm / software / components / tactics / paramodulation / inference.mli

diff --git a/helm/software/components/tactics/paramodulation/inference.mli b/helm/software/components/tactics/paramodulation/inference.mli
index 107e3b81911ca470d0422b190811e692947afa52..b08054ca4f2c90c72dc97ade2d53e493b8ed0260 100644 (file)
--- 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