parameter sintax added to axiom statement

[helm.git] / helm / software / components / ng_kernel / nCicTypeChecker.ml

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 0b4b95eba3dd2bc58d92b12056c47589791abf43..ccbebc27164a16afb088bfa131a252dca37fe472 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -659,7 +659,7 @@ and check_allowed_sort_elimination ~subst ~metasenv r =
            (PP.ppterm ~subst ~metasenv ~context so)
            )));
          (match arity1, R.whd ~subst ((name,C.Decl so)::context) ta with
-           | C.Sort s1, C.Sort s2 ->
+           | C.Sort s1, (C.Sort s2 as arity2) ->
                (match NCicEnvironment.allowed_sort_elimination s1 s2 with
                | `Yes -> ()
                | `UnitOnly ->
@@ -680,7 +680,11 @@ and check_allowed_sort_elimination ~subst ~metasenv r =
                      is_non_informative ~metasenv ~subst leftno constrty))
                 then
                  raise (TypeCheckerFailure (lazy
-                  ("Sort elimination not allowed"))))
+                  ("Sort elimination not allowed: " ^ 
+                   NCicPp.ppterm ~metasenv ~subst ~context arity1 
+                   ^ " towards "^
+                   NCicPp.ppterm ~metasenv ~subst ~context arity2
+                 ))))
            | _ -> ())
       | _,_ -> ()
   in
@@ -1052,10 +1056,7 @@ and is_really_smaller
     is_really_smaller r_uri r_len ~subst ~metasenv (shift_k (name,C.Decl s) k) t
  | C.Appl (he::_) ->
     is_really_smaller r_uri r_len ~subst ~metasenv k he
- | C.Rel _ 
- | C.Const (Ref.Ref (_,Ref.Con _)) -> false
- | C.Appl [] 
- | C.Const (Ref.Ref (_,Ref.Fix _)) -> assert false
+ | C.Appl [] | C.Implicit _ -> assert false
  | C.Meta _ -> true 
  | C.Match (Ref.Ref (_,Ref.Ind (isinductive,_,_)),_,term,pl) ->
     (match term with
@@ -1073,7 +1074,7 @@ and is_really_smaller
              is_really_smaller r_uri r_len ~subst ~metasenv k e)
            pl dcl
     | _ -> List.for_all (is_really_smaller r_uri r_len ~subst ~metasenv k) pl)
- | _ -> assert false
+ | _ -> false
 
 and returns_a_coinductive ~subst context ty =
   match R.whd ~subst context ty with
@@ -1307,7 +1308,9 @@ let typecheck_obj (uri,height,metasenv,subst,kind) =
             | C.Appl (C.Const (Ref.Ref (uri,Ref.Ind _) as ref) :: _) ->
                 let _,_,itl,_,_ = E.get_checked_indtys ref in
                   uri, List.length itl
-            | _ -> assert false
+            | _ ->
+              raise (TypeCheckerFailure
+               (lazy "Fix: the recursive argument is not inductive"))
           in
           (* guarded by destructors conditions D{f,k,x,M} *)
           let rec enum_from k =