]> matita.cs.unibo.it Git - helm.git/commitdiff
allowed sort elim now check for recursive types
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 30 Jul 2008 15:19:04 +0000 (15:19 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 30 Jul 2008 15:19:04 +0000 (15:19 +0000)
helm/software/components/cic_proof_checking/cicTypeChecker.ml

index fa24119b303babd1f406ee71558b81b5a8a7f27d..111d20126e0bba1f59272d61c493e452d7a3ccf9 100644 (file)
@@ -1179,7 +1179,9 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
              in
               (* is it a singleton or empty non recursive and non informative
                  definition? *)
-              non_informative, ugraph
+              non_informative &&
+               does_not_occur [Some (C.Name name,C.Decl ty)] 0 1
+                (debrujin_constructor uri 1 [] (snd (List.nth cl 0))), ugraph
             else
               false,ugraph
          | _ ->