fixes (mainly) to demodulation and meta_convertibility

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

diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml
index 8d97e0c4bbb8ca198d2ecf9fb449527432edac13..7f0a8ba5537e82e933b7e71cd62bd0a3b21dcc17 100644 (file)
--- a/helm/ocaml/paramodulation/utils.ml
+++ b/helm/ocaml/paramodulation/utils.ml
@@ -27,20 +27,21 @@ let string_of_weight (cw, mw) =
   Printf.sprintf "[%d; %s]" cw s
 
 
-let weight_of_term term =
+let weight_of_term ?(consider_metas=true) term =
   (* ALB: what to consider as a variable? I think "variables" in our case are
      Metas and maybe Rels... *)
   let module C = Cic in
   let vars_dict = Hashtbl.create 5 in
   let rec aux = function
-    | C.Meta (metano, _) ->
+    | C.Meta (metano, _) when consider_metas ->
         (try
            let oldw = Hashtbl.find vars_dict metano in
            Hashtbl.replace vars_dict metano (oldw+1)
          with Not_found ->
            Hashtbl.add vars_dict metano 1);
         0
-          
+    | C.Meta _ -> 0 (* "variables" are lighter than constants and functions...*)
+                  
     | C.Var (_, ens)
     | C.Const (_, ens)
     | C.MutInd (_, _, ens)