From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 30 Jul 2008 22:41:05 +0000 (+0000)
Subject: fixed check, if 0 constructors then no List.nth is allowed
X-Git-Tag: make_still_working~4869
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c63d363ae3e92ca53e7ad010d2efbd69a0c6daae;p=helm.git

fixed check, if 0 constructors then no List.nth is allowed
---

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 111d20126..7fed3ddf3 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -1174,14 +1174,17 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
              let non_informative,ugraph =
               if cl_len = 0 then true,ugraph
               else
-               is_non_informative ~logger [Some (C.Name name,C.Decl ty)]
-                paramsno (snd (List.nth cl 0)) ugraph
+               let b, ug =
+                is_non_informative ~logger [Some (C.Name name,C.Decl ty)]
+                 paramsno (snd (List.nth cl 0)) ugraph
+               in
+                b && 
+               does_not_occur [Some (C.Name name,C.Decl ty)] 0 1
+                (debrujin_constructor uri 1 [] (snd (List.nth cl 0))), ug
              in
               (* is it a singleton or empty non recursive and non informative
                  definition? *)
-              non_informative &&
-               does_not_occur [Some (C.Name name,C.Decl ty)] 0 1
-                (debrujin_constructor uri 1 [] (snd (List.nth cl 0))), ugraph
+              non_informative, ugraph
             else
               false,ugraph
          | _ ->