freescale porting, work in progress

[helm.git] / helm / software / components / ng_refiner / nCicMetaSubst.ml

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 496648f55a90460fa8fc23a297927d258e59785e..421194abdb02b3a4431149b995e6b7493e104248 100644 (file)
--- 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