X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicMetaSubst.ml;h=dd3485df093fb799b70dfb1175fdad50ff6d832a;hb=765189dfcb70fc21d14c4fdf80b6f0e0c311ee56;hp=5e72d90c77eac85827b0cef8ae790b9f51b40396;hpb=2b1eb6d5cd2d3ff5024e48615df4b99692008690;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 5e72d90c7..dd3485df0 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -363,10 +363,10 @@ let mk_meta ?name metasenv context ty =
     mk_meta name (newmeta ()) metasenv context ty
 ;;
 
-let saturate ?(delta=0) metasenv context ty goal_arity =
+let saturate ?(delta=0) metasenv subst context ty goal_arity =
  assert (goal_arity >= 0);
   let rec aux metasenv = function
-   | NCic.Prod (name,s,t) ->
+   | NCic.Prod (name,s,t) as ty ->
        let metasenv1, arg,_ = 
           mk_meta ~name:name metasenv context (`WithType s) in            
        let t, metasenv1, args, pno = 
@@ -377,7 +377,7 @@ let saturate ?(delta=0) metasenv context ty goal_arity =
        else
          t, metasenv1, arg::args, pno+1
    | ty ->
-        match NCicReduction.whd context ty ~delta with
+        match NCicReduction.whd ~subst context ty ~delta with
         | NCic.Prod _ as ty -> aux metasenv ty
         | ty -> ty, metasenv, [], 0
   in