X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Futils.mli;h=2f1533e69260638ca834789e2820ff46732bc4b2;hb=ec7717f5e0dd4c295ba1cfd57a0a6a46170490ef;hp=f44cab460ee5837043e07cfc29eb23a5f7d5fbe7;hpb=d1161f58d1537528aa2810706819f5251a0954d9;p=helm.git diff --git a/components/tactics/paramodulation/utils.mli b/components/tactics/paramodulation/utils.mli index f44cab460..2f1533e69 100644 --- a/components/tactics/paramodulation/utils.mli +++ b/components/tactics/paramodulation/utils.mli @@ -87,6 +87,7 @@ val compute_equality_weight: Cic.term * Cic.term * Cic.term * comparison -> int val debug_print: string Lazy.t -> unit +val eq_URI: unit -> UriManager.uri val eq_ind_URI: unit -> UriManager.uri val eq_ind_r_URI: unit -> UriManager.uri val sym_eq_URI: unit -> UriManager.uri