From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 9 Dec 2008 16:04:20 +0000 (+0000)
Subject: saturate was not returning the correct (saturated) type (but a correct number
X-Git-Tag: make_still_working~4428
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e1194dc5441516b1ab6dfaa4a0bf8915a6874ffc;p=helm.git

saturate was not returning the correct (saturated) type (but a correct number
of arguments.
---

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 =