]> matita.cs.unibo.it Git - helm.git/commitdiff
To check if a term is type, do a whd of its sort before matching it.
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 15 Dec 2008 13:26:26 +0000 (13:26 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 15 Dec 2008 13:26:26 +0000 (13:26 +0000)
helm/software/components/cic_unification/cicRefine.ml

index 0168d2d7573493a91fc67891b43b71ee0e48270f..7b26cf6db06e0666c1f92dda0e8f3bd2020bf675 100644 (file)
@@ -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 *)