X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=421194abdb02b3a4431149b995e6b7493e104248;hb=d00e19c7000a00659ffd609ef79675eb0f010659;hp=496648f55a90460fa8fc23a297927d258e59785e;hpb=7b112b0cd39c5ab0db5c28636c0a7f7e36b4d6e2;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 496648f55..421194abd 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -207,11 +207,18 @@ and restrict metasenv subst i restrictions =
 ;;
 
 let rec flexible_arg context subst = function 
-  | NCic.Meta (i,_) | NCic.Appl (NCic.Meta (i,_) :: _)-> 
+  | NCic.Meta (i,_) ->
       (try 
         let _,_,t,_ = List.assoc i subst in
         flexible_arg context subst t
       with Not_found -> true)
+  | NCic.Appl (NCic.Meta (i,_) :: args)-> 
+      (try 
+        let _,_,t,_ = List.assoc i subst in
+        flexible_arg context subst 
+          (NCicReduction.head_beta_reduce ~delta:max_int 
+            (NCic.Appl (t :: args)))
+      with Not_found -> true)
    (* this is a cheap whd, it only performs zeta-reduction.
     * 
     * it works when the **omissis** disambiguation algorithm