From 48794769c34c57e3ead42edc8c8eca5333e857ea Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 6 Nov 2008 14:06:00 +0000 Subject: [PATCH] do not erase sorts --- helm/software/components/ng_refiner/check.ml | 2 ++ 1 file changed, 2 insertions(+) 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) -- 2.39.2