From e1194dc5441516b1ab6dfaa4a0bf8915a6874ffc Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 9 Dec 2008 16:04:20 +0000
Subject: [PATCH] saturate was not returning the correct (saturated) type (but
 a correct number of arguments.

---
 helm/software/components/ng_refiner/nCicMetaSubst.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 = 
-- 
2.39.2