]> matita.cs.unibo.it Git - helm.git/commitdiff
saturate was not returning the correct (saturated) type (but a correct number
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 9 Dec 2008 16:04:20 +0000 (16:04 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 9 Dec 2008 16:04:20 +0000 (16:04 +0000)
of arguments.

helm/software/components/ng_refiner/nCicMetaSubst.ml

index 6a0406747abba552d2811eb2337b44055b79d83a..dd3485df093fb799b70dfb1175fdad50ff6d832a 100644 (file)
@@ -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 =