X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=d51ce368582efc41e1084bb84e780ad4bd7d041c;hb=926bd86002f91d2bf2a3ce7376309f5106268959;hp=beeeeeb6b288a6c22cc0d8bfe28efd67c31066ef;hpb=66be8fbe19e2ccfa0e6a7abeba605152d1322595;p=helm.git

diff --git a/matita/components/ng_refiner/nCicMetaSubst.ml b/matita/components/ng_refiner/nCicMetaSubst.ml
index beeeeeb6b..d51ce3685 100644
--- a/matita/components/ng_refiner/nCicMetaSubst.ml
+++ b/matita/components/ng_refiner/nCicMetaSubst.ml
@@ -221,7 +221,7 @@ and restrict status metasenv subst i (restrictions as orig) =
         let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
         let new_subst = 
           subst_entry_j :: List.map 
-            (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst
+            (fun ((n,_) as orig) -> if i = n then subst_entry_i else orig) subst
         in
         let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in
         metasenv, new_subst, j, diff
@@ -250,7 +250,7 @@ and restrict status metasenv subst i (restrictions as orig) =
           pp (lazy ("BBB: dopo metasenv\n" ^  NCicPp.ppmetasenv ~subst [metasenv_entry]));*)
         let diff = List.filter (fun x -> not (List.mem x orig)) restrictions in
         List.map 
-          (fun (n,_) as orig -> if i = n then metasenv_entry else orig) 
+          (fun ((n,_) as orig) -> if i = n then metasenv_entry else orig) 
           metasenv,
         subst_entry :: subst, j, diff
       with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
@@ -390,7 +390,7 @@ let delift status ~unify metasenv subst context n l t =
              if not clear then ms
              else 
                metasenv, 
-               (i,([],c,t,ty)) :: List.filter (fun j,_ -> i <> j) subst
+               (i,([],c,t,ty)) :: List.filter (fun (j,_) -> i <> j) subst
            in
            aux (context,k,in_scope) ms (NCicSubstitution.subst_meta status l1 t)
          with NCicUtils.Subst_not_found _ ->
@@ -572,7 +572,7 @@ let extend_meta metasenv n =
   | NCic.Implicit (`Typeof _) -> 
       let mk_meta context kind =
         let metasenv, _, ty, _ = mk_meta metasenv context kind in
-        (n, (attrs, cc, ty)) :: List.filter (fun x,_ -> x <> n) metasenv, ty
+        (n, (attrs, cc, ty)) :: List.filter (fun (x,_) -> x <> n) metasenv, ty
       in
       (match NCicUntrusted.kind_of_meta attrs with
        | `IsSort