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=6a0406747abba552d2811eb2337b44055b79d83a;hpb=002d456397be2f0046bb50356e80816f7296647d;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index 6a0406747..dd3485df0 100644
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -366,7 +366,7 @@ let mk_meta ?name metasenv context ty =
 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 =