X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_paramodulation%2FfoUnif.ml;h=c6d1305126d9a80177ec61d3d52f3898578f465b;hb=3220eee6c3dd2968727c5c595d6ca78e89291b5f;hp=0946873b9af5c11fea237022b2394a40393e3de6;hpb=cf8b1c25a0011ca2a8a856b39e046da33c451221;p=helm.git

diff --git a/matita/components/ng_paramodulation/foUnif.ml b/matita/components/ng_paramodulation/foUnif.ml
index 0946873b9..c6d130512 100644
--- a/matita/components/ng_paramodulation/foUnif.ml
+++ b/matita/components/ng_paramodulation/foUnif.ml
@@ -58,12 +58,12 @@ module Founif (B : Orderings.Blob) = struct
             Subst.build_subst i t subst
       | Terms.Var i, t when occurs_check subst i t ->
           raise (UnificationFailure (lazy "Inference.unification.unif"))
-      | Terms.Var i, t when (List.mem i locked_vars) -> 
+      | Terms.Var i, _t when (List.mem i locked_vars) -> 
           raise (UnificationFailure (lazy "Inference.unification.unif"))
       | Terms.Var i, t -> Subst.build_subst i t subst
       | t, Terms.Var i when occurs_check subst i t ->
           raise (UnificationFailure (lazy "Inference.unification.unif"))
-      | t, Terms.Var i when (List.mem i locked_vars) -> 
+      | _t, Terms.Var i when (List.mem i locked_vars) -> 
           raise (UnificationFailure (lazy "Inference.unification.unif"))
       | t, Terms.Var i -> Subst.build_subst i t subst
       | Terms.Node l1, Terms.Node l2 -> (
@@ -90,7 +90,7 @@ module Founif (B : Orderings.Blob) = struct
       in
       match s, t with
         | s, t when U.eq_foterm s t -> subst
-        | Terms.Var i, Terms.Var j
+        | Terms.Var i, Terms.Var _j
             when (not (List.exists (fun (_,k) -> k=t) subst)) ->
             let subst = Subst.build_subst i t subst in
               subst