From 567275a08875a20fa417429ecceb62df70ecbd53 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 15 Dec 2008 13:26:26 +0000
Subject: [PATCH] To check if a term is type, do a whd of its sort before
 matching it.

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

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 0168d2d75..7b26cf6db 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -1985,7 +1985,7 @@ let typecheck metasenv uri obj ~localization_tbl =
      let ty',sort,metasenv,ugraph =
       type_of_aux' ~localization_tbl metasenv [] ty ugraph in
      begin
-      match sort with
+       match CicReduction.whd ~delta:true [] sort with
          Cic.Sort _
        (* instead of raising Uncertain, let's hope that the meta will become
           a sort *)
-- 
2.39.2