From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 6 Nov 2008 14:06:00 +0000 (+0000)
Subject: do not erase sorts
X-Git-Tag: make_still_working~4590
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=48794769c34c57e3ead42edc8c8eca5333e857ea;p=helm.git

do not erase sorts
---

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 7d13b9a35..d4a329697 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -226,6 +226,8 @@ let _ =
                  (fun e ctx -> e::ctx) ctx perforate metasenv t
           in
           let rec curryfy ctx = function
+            | NCic.Lambda (name, (NCic.Sort _ as s), tgt) ->
+                NCic.Lambda (name, s, curryfy ((name,NCic.Decl s) :: ctx) tgt)
             | NCic.Lambda (name, s, tgt) ->
                 let tgt = curryfy ((name,NCic.Decl s) :: ctx) tgt in
                 NCic.Lambda (name, NCic.Implicit `Type, tgt)