fixes (mainly) to demodulation and meta_convertibility

[helm.git] / helm / ocaml / paramodulation / utils.mli

diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli
index 164d4f303b8fde4cc44371ee9c7c7a9b977172cd..235085ab149eb488b9507af12412414f7aff19cc 100644 (file)
--- a/helm/ocaml/paramodulation/utils.mli
+++ b/helm/ocaml/paramodulation/utils.mli
@@ -9,7 +9,7 @@ val print_subst: Cic.substitution -> string
 
 val string_of_weight: weight -> string
 
-val weight_of_term: Cic.term -> weight
+val weight_of_term: ?consider_metas:bool -> Cic.term -> weight
 
 val normalize_weight: int -> weight -> weight