X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=549f06f85b57845c97737b609855b5b95fd016cc;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=b18364509db79f282b7d18372bee0d2cd189f87c;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index b18364509..549f06f85 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -259,16 +259,16 @@ and restrict metasenv subst i (restrictions as orig) =
     | NCicUtils.Meta_not_found _ -> assert false
 ;;
 
-let rec is_flexible context ~subst = function 
+let rec flexible_arg context subst = function 
   | NCic.Meta (i,_) ->
       (try 
         let _,_,t,_ = List.assoc i subst in
-        is_flexible context ~subst t
+        flexible_arg context subst t
       with Not_found -> true)
   | NCic.Appl (NCic.Meta (i,_) :: args)-> 
       (try 
         let _,_,t,_ = List.assoc i subst in
-        is_flexible context ~subst 
+        flexible_arg context subst 
           (NCicReduction.head_beta_reduce ~delta:max_int 
             (NCic.Appl (t :: args)))
       with Not_found -> true)
@@ -283,7 +283,7 @@ let rec is_flexible context ~subst = function
          match List.nth context (i-1)
          with 
          | _,NCic.Def (bo,_) ->
-               is_flexible context ~subst
+               flexible_arg context subst
                  (NCicSubstitution.lift i bo)
          | _ -> false
       with 
@@ -332,11 +332,11 @@ let delift ~unify metasenv subst context n l t =
     match l with
     | _, NCic.Irl _ -> fun _ _ _ _ _ -> None
     | shift, NCic.Ctx l -> fun metasenv subst context k t ->
-       if is_flexible context ~subst t || contains_in_scope subst t then None else
+       if flexible_arg context subst t || contains_in_scope subst t then None else
          let lb = 
            List.map (fun t -> 
             let t = NCicSubstitution.lift (k+shift) t in
-            t, is_flexible context ~subst t) 
+            t, flexible_arg context subst t) 
            l 
          in
          HExtlib.list_findopt