X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=951f68dbd84b28043a100fe3c72c114d4f5927a7;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=007962097e03b95c2f8318937e8f93f30f61e4b9;hpb=e174574339e22f1d6a518f9b272ad412a0cd7a90;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 007962097..951f68dbd 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -23,13 +23,15 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 (* TODO factorize functions to frequent errors (e.g. "Unknwon mutual inductive
  * ...") *)
 
 open Printf
 
-exception AssertFailure of string;;
-exception TypeCheckerFailure of string;;
+exception AssertFailure of string Lazy.t;;
+exception TypeCheckerFailure of string Lazy.t;;
 
 let fdebug = ref 0;;
 let debug t context =
@@ -39,26 +41,27 @@ let debug t context =
    CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
  in
   if !fdebug = 0 then
-   raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) ""))
+   raise (TypeCheckerFailure (lazy (List.fold_right debug_aux (t::context) "")))
 ;;
 
-let debug_print = fun _ -> () ;;
+let debug_print = fun _ -> ();;
 
 let rec split l n =
  match (l,n) with
     (l,0) -> ([], l)
   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
   | (_,_) ->
-      raise (TypeCheckerFailure "Parameters number < left parameters number")
+      raise (TypeCheckerFailure (lazy "Parameters number < left parameters number"))
 ;;
 
-let debrujin_constructor uri number_of_types =
- let rec aux k =
+let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
+ let rec aux k t =
   let module C = Cic in
-   function
+  let res =
+   match t with
       C.Rel n as t when n <= k -> t
     | C.Rel _ ->
-        raise (TypeCheckerFailure "unbound variable found in constructor type")
+        raise (TypeCheckerFailure (lazy "unbound variable found in constructor type"))
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst' = 
         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
@@ -66,7 +69,7 @@ let debrujin_constructor uri number_of_types =
         C.Var (uri,exp_named_subst')
     | C.Meta (i,l) ->
        let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in
-        C.Meta (i,l)
+        C.Meta (i,l')
     | C.Sort _
     | C.Implicit _ as t -> t
     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
@@ -82,8 +85,8 @@ let debrujin_constructor uri number_of_types =
     | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
        if exp_named_subst != [] then
         raise (TypeCheckerFailure
-          ("non-empty explicit named substitution is applied to "^
-           "a mutual inductive type which is being defined")) ;
+          (lazy ("non-empty explicit named substitution is applied to "^
+           "a mutual inductive type which is being defined"))) ;
        C.Rel (k + number_of_types - tyno) ;
     | C.MutInd (uri',tyno,exp_named_subst) ->
        let exp_named_subst' = 
@@ -114,6 +117,9 @@ let debrujin_constructor uri number_of_types =
           fl
        in
         C.CoFix (i, liftedfl)
+  in
+   cb t res;
+   res
  in
   aux 0
 ;;
@@ -143,10 +149,10 @@ let rec type_of_constant ~logger uri ugraph =
            let type_of_te,ugraph' = type_of ~logger te ugraph in
               let b',ugraph'' = (R.are_convertible [] type_of_te ty ugraph') in
               if not b' then
-               raise (TypeCheckerFailure (sprintf
+               raise (TypeCheckerFailure (lazy (sprintf
                 "the constant %s is not well typed because the type %s of the body is not convertible to the declared type %s"
                 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
-                (CicPp.ppterm ty)))
+                (CicPp.ppterm ty))))
               else
                 ugraph'
          | C.Constant (_,None,ty,_,_) ->
@@ -169,15 +175,15 @@ let rec type_of_constant ~logger uri ugraph =
 	       in
                let b,ugraph4 = (R.are_convertible [] type_of_te ty ugraph3) in
                if not b then
-                 raise (TypeCheckerFailure (sprintf
+                 raise (TypeCheckerFailure (lazy (sprintf
                   "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
                   (U.string_of_uri uri) (CicPp.ppterm type_of_te)
-                  (CicPp.ppterm ty)))
+                  (CicPp.ppterm ty))))
                else 
                  ugraph4
          | _ ->
-             raise (TypeCheckerFailure
-		      ("Unknown constant:" ^ U.string_of_uri uri))) 
+             raise
+              (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri))))
        in 
 	 try
 	   CicEnvironment.set_type_checking_info uri;
@@ -193,7 +199,7 @@ let rec type_of_constant ~logger uri ugraph =
       (C.Constant (_,_,ty,_,_)),g -> ty,g
     | (C.CurrentProof (_,_,_,ty,_,_)),g -> ty,g
     | _ ->
-        raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri))
+        raise (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri)))
 
 and type_of_variable ~logger uri ugraph =
  let module C = Cic in
@@ -214,7 +220,7 @@ and type_of_variable ~logger uri ugraph =
              let b,ugraph'' = (R.are_convertible [] ty_bo ty ugraph') in
              if not b then
               raise (TypeCheckerFailure
-                ("Unknown variable:" ^ U.string_of_uri uri))
+                (lazy ("Unknown variable:" ^ U.string_of_uri uri)))
 	     else
 	       ugraph'') 
       in
@@ -230,7 +236,7 @@ and type_of_variable ~logger uri ugraph =
            (*debug_print (lazy s);*)
            ty,ugraph2)
    |  _ ->
-	raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
+	raise (TypeCheckerFailure (lazy ("Unknown variable:" ^ U.string_of_uri uri)))
 
 and does_not_occur ?(subst=[]) context n nn te =
  let module C = Cic in
@@ -382,7 +388,7 @@ and weakly_positive context n nn uri te =
        weakly_positive ((Some (name,(C.Decl source)))::context)
         (n + 1) (nn + 1) uri dest
    | _ ->
-     raise (TypeCheckerFailure "Malformed inductive constructor type")
+     raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
 
 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
@@ -394,7 +400,7 @@ and instantiate_parameters params c =
        instantiate_parameters tl
         (CicSubstitution.subst he ta)
    | (C.Cast (te,_), _) -> instantiate_parameters params te
-   | (t,l) -> raise (AssertFailure "1")
+   | (t,l) -> raise (AssertFailure (lazy "1"))
 
 and strictly_positive context n nn te =
  let module C = Cic in
@@ -418,7 +424,7 @@ and strictly_positive context n nn te =
              (List.length tl = 1, paramsno, ity, cl, name)
          | _ ->
            raise (TypeCheckerFailure
-            ("Unknown inductive type:" ^ U.string_of_uri uri))
+            (lazy ("Unknown inductive type:" ^ U.string_of_uri uri)))
       in
        let (params,arguments) = split tl paramsno in
        let lifted_params = List.map (CicSubstitution.lift 1) params in
@@ -460,23 +466,24 @@ and are_all_occurrences_positive context uri indparamsno i n nn te =
               C.Rel m when m = n - (indparamsno - k) -> k - 1
             | _ ->
               raise (TypeCheckerFailure
-                ("Non-positive occurence in mutual inductive definition(s) " ^
-                UriManager.string_of_uri uri))
+               (lazy 
+               ("Non-positive occurence in mutual inductive definition(s) [1]" ^
+                UriManager.string_of_uri uri)))
         ) indparamsno tl
       in
        if last = 0 then
         List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
        else
         raise (TypeCheckerFailure
-          ("Non-positive occurence in mutual inductive definition(s) " ^
-          UriManager.string_of_uri uri))
+         (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
+          UriManager.string_of_uri uri)))
    | C.Rel m when m = i ->
       if indparamsno = 0 then
        true
       else
         raise (TypeCheckerFailure
-          ("Non-positive occurence in mutual inductive definition(s) " ^
-          UriManager.string_of_uri uri))
+         (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
+          UriManager.string_of_uri uri)))
    | C.Prod (C.Anonymous,source,dest) ->
       strictly_positive context n nn source &&
        are_all_occurrences_positive
@@ -495,8 +502,8 @@ and are_all_occurrences_positive context uri indparamsno i n nn te =
         uri indparamsno (i+1) (n + 1) (nn + 1) dest
    | _ ->
      raise
-      (TypeCheckerFailure ("Malformed inductive constructor type " ^
-        (UriManager.string_of_uri uri)))
+      (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^
+        (UriManager.string_of_uri uri))))
 
 (* Main function to checks the correctness of a mutual *)
 (* inductive block definition. This is the function    *)
@@ -538,13 +545,13 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
                      debrujinedte)
               then
 		raise
-		  (TypeCheckerFailure ("Non positive occurence in " ^
-				       U.string_of_uri uri))
+		  (TypeCheckerFailure
+                    (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))
               else
 		ugraph'
             ) ugraph cl in
 	(i + 1),ugraph''
-      ) itl (1,ugraph)
+      ) itl (1,ugrap1)
   in
   ugraph2
 
@@ -556,8 +563,8 @@ and check_mutual_inductive_defs uri obj ugraph =
 	typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph 
     | _ ->
 	raise (TypeCheckerFailure (
-		 "Unknown mutual inductive definition:" ^
-		 UriManager.string_of_uri uri))
+		lazy ("Unknown mutual inductive definition:" ^
+		 UriManager.string_of_uri uri)))
 
 and type_of_mutual_inductive_defs ~logger uri i ugraph =
  let module C = Cic in
@@ -589,8 +596,8 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph =
 	  let (_,_,arity,_) = List.nth dl i in
 	    arity,ugraph1
       | _ ->
-	  raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
-				     U.string_of_uri uri))
+	  raise (TypeCheckerFailure
+           (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri)))
 	    
 and type_of_mutual_inductive_constr ~logger uri i j ugraph =
  let module C = Cic in
@@ -625,8 +632,8 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph =
           let (_,ty) = List.nth cl (j-1) in
             ty,ugraph1
       | _ ->
-	  raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
-				     UriManager.string_of_uri uri))
+	  raise (TypeCheckerFailure
+           (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)))
 
 and recursive_args context n nn te =
  let module C = Cic in
@@ -637,20 +644,20 @@ and recursive_args context n nn te =
    | C.Sort _
    | C.Implicit _
    | C.Cast _ (*CSC ??? *) ->
-      raise (AssertFailure "3") (* due to type-checking *)
+      raise (AssertFailure (lazy "3")) (* due to type-checking *)
    | C.Prod (name,so,de) ->
       (not (does_not_occur context n nn so)) ::
        (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
    | C.Lambda _
    | C.LetIn _ ->
-      raise (AssertFailure "4") (* due to type-checking *)
+      raise (AssertFailure (lazy "4")) (* due to type-checking *)
    | C.Appl _ -> []
-   | C.Const _ -> raise (AssertFailure "5")
+   | C.Const _ -> raise (AssertFailure (lazy "5"))
    | C.MutInd _
    | C.MutConstruct _
    | C.MutCase _
    | C.Fix _
-   | C.CoFix _ -> raise (AssertFailure "6") (* due to type-checking *)
+   | C.CoFix _ -> raise (AssertFailure (lazy "6")) (* due to type-checking *)
 
 and get_new_safes ~subst context p c rl safes n nn x =
  let module C = Cic in
@@ -679,9 +686,9 @@ and get_new_safes ~subst context p c rl safes n nn x =
       (* CSC: particular, this means that a new (C.Prod, x,_) case  *)
       (* CSC: must be considered in this match. (e.g. x = MutCase)  *)
       raise
-       (AssertFailure
+       (AssertFailure (lazy
          (Printf.sprintf "Get New Safes: c=%s ; p=%s"
-           (CicPp.ppterm c) (CicPp.ppterm p)))
+           (CicPp.ppterm c) (CicPp.ppterm p))))
 
 and split_prods ~subst context n te =
  let module C = Cic in
@@ -690,7 +697,7 @@ and split_prods ~subst context n te =
      (0, _) -> context,te
    | (n, C.Prod (name,so,ta)) when n > 0 ->
        split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
-   | (_, _) -> raise (AssertFailure "8")
+   | (_, _) -> raise (AssertFailure (lazy "8"))
 
 and eat_lambdas ~subst context n te =
  let module C = Cic in
@@ -703,7 +710,7 @@ and eat_lambdas ~subst context n te =
       in
        (te, k + 1, context')
    | (n, te) ->
-       raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))
+       raise (AssertFailure (lazy (sprintf "9 (%d, %s)" n (CicPp.ppterm te))))
 
 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) 
 and check_is_really_smaller_arg ~subst context n nn kl x safes te =
@@ -726,7 +733,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
       check_is_really_smaller_arg ~subst n nn kl x safes so &&
        check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1)
         (List.map (fun x -> x + 1) safes) ta*)
-   | C.Prod _ -> raise (AssertFailure "10")
+   | C.Prod _ -> raise (AssertFailure (lazy "10"))
    | C.Lambda (name,so,ta) ->
       check_is_really_smaller_arg ~subst context n nn kl x safes so &&
        check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context)
@@ -739,9 +746,9 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
       (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
       (*CSC: solo perche' non abbiamo trovato controesempi            *)
       check_is_really_smaller_arg ~subst context n nn kl x safes he
-   | C.Appl [] -> raise (AssertFailure "11")
+   | C.Appl [] -> raise (AssertFailure (lazy "11"))
    | C.Const _
-   | C.MutInd _ -> raise (AssertFailure "12")
+   | C.MutInd _ -> raise (AssertFailure (lazy "12"))
    | C.MutConstruct _ -> false
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match term with
@@ -763,8 +770,8 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                    (tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
-                  ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri))
+                  (lazy ("Unknown mutual inductive definition:" ^
+                  UriManager.string_of_uri uri)))
            in
             if not isinductive then
               List.fold_right
@@ -777,7 +784,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                List.combine pl cl
               with
                Invalid_argument _ ->
-                raise (TypeCheckerFailure "not enough patterns")
+                raise (TypeCheckerFailure (lazy "not enough patterns"))
              in
               List.fold_right
                (fun (p,(_,c)) i ->
@@ -809,8 +816,8 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                    (tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
-                  ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri))
+                  (lazy ("Unknown mutual inductive definition:" ^
+                  UriManager.string_of_uri uri)))
            in
             if not isinductive then
               List.fold_right
@@ -823,7 +830,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te =
                List.combine pl cl
               with
                Invalid_argument _ ->
-                raise (TypeCheckerFailure "not enough patterns")
+                raise (TypeCheckerFailure (lazy "not enough patterns"))
              in
               (*CSC: supponiamo come prima che nessun controllo sia necessario*)
               (*CSC: sugli argomenti di una applicazione                      *)
@@ -883,7 +890,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
         | Some (_,C.Def (bo,_)) ->
            guarded_by_destructors ~subst context m nn kl x safes
             (CicSubstitution.lift m bo)
-        | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
+        | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
       )
    | C.Meta _
    | C.Sort _
@@ -947,8 +954,8 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                     (tys,len,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
-                  ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri))
+                  (lazy ("Unknown mutual inductive definition:" ^
+                  UriManager.string_of_uri uri)))
            in
             if not isinductive then
              guarded_by_destructors ~subst context n nn kl x safes outtype &&
@@ -964,7 +971,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                List.combine pl cl
               with
                Invalid_argument _ ->
-                raise (TypeCheckerFailure "not enough patterns")
+                raise (TypeCheckerFailure (lazy "not enough patterns"))
              in
              guarded_by_destructors ~subst context n nn kl x safes outtype &&
               (*CSC: manca ??? il controllo sul tipo di term? *)
@@ -995,8 +1002,8 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                    (tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
                 raise (TypeCheckerFailure
-                  ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri))
+                  (lazy ("Unknown mutual inductive definition:" ^
+                  UriManager.string_of_uri uri)))
            in
             if not isinductive then
              guarded_by_destructors ~subst context n nn kl x safes outtype &&
@@ -1012,7 +1019,7 @@ and guarded_by_destructors ~subst context n nn kl x safes =
                List.combine pl cl
               with
                Invalid_argument _ ->
-                raise (TypeCheckerFailure "not enough patterns")
+                raise (TypeCheckerFailure (lazy "not enough patterns"))
              in
              guarded_by_destructors ~subst context n nn kl x safes outtype &&
               (*CSC: manca ??? il controllo sul tipo di term? *)
@@ -1086,7 +1093,7 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
    | C.Prod _
    | C.LetIn _ ->
       (* the term has just been type-checked *)
-      raise (AssertFailure "17")
+      raise (AssertFailure (lazy "17"))
    | C.Lambda (name,so,de) ->
       does_not_occur ~subst context n nn so &&
        guarded_by_constructors ~subst ((Some (name,(C.Decl so)))::context)
@@ -1107,46 +1114,45 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
             let (_,cons) = List.nth cl (j - 1) in
              CicSubstitution.subst_vars exp_named_subst cons
         | _ ->
-            raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
-              UriManager.string_of_uri uri))
+            raise (TypeCheckerFailure
+             (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)))
       in
        let rec analyse_branch context ty te =
         match CicReduction.whd ~subst context ty with
-           C.Meta _ -> raise (AssertFailure "34")
+           C.Meta _ -> raise (AssertFailure (lazy "34"))
          | C.Rel _
          | C.Var _
          | C.Sort _ ->
             does_not_occur ~subst context n nn te
          | C.Implicit _
          | C.Cast _ ->
-            raise (AssertFailure "24")(* due to type-checking *)
+            raise (AssertFailure (lazy "24"))(* due to type-checking *)
          | C.Prod (name,so,de) ->
             analyse_branch ((Some (name,(C.Decl so)))::context) de te
          | C.Lambda _
          | C.LetIn _ ->
-            raise (AssertFailure "25")(* due to type-checking *)
-         | C.Appl ((C.MutInd (uri,_,_))::_) as ty
-            when uri == coInductiveTypeURI -> 
+            raise (AssertFailure (lazy "25"))(* due to type-checking *)
+         | C.Appl ((C.MutInd (uri,_,_))::_) when uri == coInductiveTypeURI -> 
              guarded_by_constructors ~subst context n nn true te []
               coInductiveTypeURI
-         | C.Appl ((C.MutInd (uri,_,_))::_) as ty -> 
+         | C.Appl ((C.MutInd (uri,_,_))::_) -> 
             guarded_by_constructors ~subst context n nn true te tl
              coInductiveTypeURI
          | C.Appl _ ->
             does_not_occur ~subst context n nn te
-         | C.Const _ -> raise (AssertFailure "26")
+         | C.Const _ -> raise (AssertFailure (lazy "26"))
          | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
             guarded_by_constructors ~subst context n nn true te []
              coInductiveTypeURI
          | C.MutInd _ ->
             does_not_occur ~subst context n nn te
-         | C.MutConstruct _ -> raise (AssertFailure "27")
+         | C.MutConstruct _ -> raise (AssertFailure (lazy "27"))
          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
          (*CSC: in head position.                                       *)
          | C.MutCase _
          | C.Fix _
          | C.CoFix _ ->
-            raise (AssertFailure "28")(* due to type-checking *)
+            raise (AssertFailure (lazy "28"))(* due to type-checking *)
        in
        let rec analyse_instantiated_type context ty l =
         match CicReduction.whd ~subst context ty with
@@ -1155,7 +1161,7 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
          | C.Meta _
          | C.Sort _
          | C.Implicit _
-         | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
+         | C.Cast _ -> raise (AssertFailure (lazy "29"))(* due to type-checking *)
          | C.Prod (name,so,de) ->
             begin
              match l with
@@ -1167,21 +1173,21 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
             end
          | C.Lambda _
          | C.LetIn _ ->
-            raise (AssertFailure "30")(* due to type-checking *)
+            raise (AssertFailure (lazy "30"))(* due to type-checking *)
          | C.Appl _ -> 
             List.fold_left
              (fun i x -> i && does_not_occur ~subst context n nn x) true l
-         | C.Const _ -> raise (AssertFailure "31")
+         | C.Const _ -> raise (AssertFailure (lazy "31"))
          | C.MutInd _ ->
             List.fold_left
              (fun i x -> i && does_not_occur ~subst context n nn x) true l
-         | C.MutConstruct _ -> raise (AssertFailure "32")
+         | C.MutConstruct _ -> raise (AssertFailure (lazy "32"))
          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
          (*CSC: in head position.                                       *)
          | C.MutCase _
          | C.Fix _
          | C.CoFix _ ->
-            raise (AssertFailure "33")(* due to type-checking *)
+            raise (AssertFailure (lazy "33"))(* due to type-checking *)
        in
         let rec instantiate_type args consty =
          function
@@ -1200,7 +1206,7 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
                     | _ ->
                       (*CSC:We do not consider backbones with a MutCase, a    *)
                       (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
-                      raise (AssertFailure "23")
+                      raise (AssertFailure (lazy "23"))
                   end
                | [] -> analyse_instantiated_type context consty' l
                   (* These are all the other cases *)
@@ -1277,7 +1283,9 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
   need_dummy ind arity1 arity2 ugraph =
  let module C = Cic in
  let module U = UriManager in
-  match (CicReduction.whd ~subst context arity1, CicReduction.whd ~subst context arity2) with
+  let arity1 = CicReduction.whd ~subst context arity1 in
+  let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy =
+   match arity1, CicReduction.whd ~subst context arity2 with
      (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
        let b,ugraph1 =
         CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in
@@ -1287,22 +1295,40 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
           ugraph1
        else
 	 false,ugraph1
+   | (C.Sort _, C.Prod (name,so,ta)) when not need_dummy ->
+       let b,ugraph1 =
+        CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
+       if not b then
+	 false,ugraph1
+       else
+        check_allowed_sort_elimination_aux ugraph1
+         ((Some (name,C.Decl so))::context) ta true
    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
    | (C.Sort C.Prop, C.Sort C.Set)
    | (C.Sort C.Prop, C.Sort C.CProp)
    | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
-   (* TASSI: da verificare *)
-(*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 	 match o with
-         C.InductiveDefinition (itl,_,_,_) ->
-           let (_,_,_,cl) = List.nth itl i in
-           (* is a singleton definition or the empty proposition? *)
-           (List.length cl = 1 || List.length cl = 0) , ugraph
+         C.InductiveDefinition (itl,_,paramsno,_) ->
+           let itl_len = List.length itl in
+           let (name,_,ty,cl) = List.nth itl i in
+           let cl_len = List.length cl in
+            if (cl_len = 0 || (itl_len = 1 && cl_len = 1)) then
+             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
+             in
+              (* is it a singleton or empty non recursive and non informative
+                 definition? *)
+              non_informative, ugraph
+            else
+              false,ugraph
          | _ ->
              raise (TypeCheckerFailure 
-		      ("Unknown mutual inductive definition:" ^
-		       UriManager.string_of_uri uri))
+		     (lazy ("Unknown mutual inductive definition:" ^
+		       UriManager.string_of_uri uri)))
        )
    | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph
    | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph
@@ -1311,7 +1337,6 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
    | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph
    | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph
    | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
-      (* TASSI: da verificare *)
       when need_dummy ->
        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 	 match o with
@@ -1328,71 +1353,14 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
 		   false,ugraph
 		    ) cl (true,ugraph))
            | _ ->
-            raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
-              UriManager.string_of_uri uri))
+            raise (TypeCheckerFailure
+             (lazy ("Unknown mutual inductive definition:" ^
+              UriManager.string_of_uri uri)))
        )
    | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
-     (* TASSI: da verificare *)
-   | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
-       let b,ugraph1 =
-        CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
-       if not b then
-	 false,ugraph1
-       else
-         (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with
-              C.Sort C.Prop -> true,ugraph1
-           | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) ->
-               (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-                 match o with
-                    C.InductiveDefinition (itl,_,_,_) ->
-                     let (_,_,_,cl) = List.nth itl i in
-                     (* is a singleton definition or the empty proposition? *)
-                     (List.length cl = 1 || List.length cl = 0),ugraph1
-                  | _ ->
-                   raise (TypeCheckerFailure
-                    ("Unknown mutual inductive definition:" ^
-                       UriManager.string_of_uri uri)))
-           | _ -> false,ugraph1)
-   | ((C.Sort C.Set, C.Prod (name,so,ta)) 
-   | (C.Sort C.CProp, C.Prod (name,so,ta)))
-     when not need_dummy ->
-       let b,ugraph1 =
-        CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
-       if not b then
-	 false,ugraph1
-       else
-         (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with
-           C.Sort C.Prop
-         | C.Sort C.Set  -> true,ugraph1
-         | C.Sort C.CProp -> true,ugraph1
-         | C.Sort (C.Type _) ->
-             (* TASSI: da verificare *)
-             (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-	       match o with
-               C.InductiveDefinition (itl,_,paramsno,_) ->
-                 let (_,_,_,cl) = List.nth itl i in
-                 let tys =
-                   List.map
-                     (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
-                 in
-                 (List.fold_right
-                   (fun (_,x) (i,ugraph) -> 
-		      if i then 
-		        is_small ~logger tys paramsno x ugraph
-	              else
-		        false,ugraph
-	           ) cl (true,ugraph1))
-             | _ ->
-                 raise (TypeCheckerFailure
-			  ("Unknown mutual inductive definition:" ^
-			   UriManager.string_of_uri uri))
-             )
-         | _ -> raise (AssertFailure "19")
-         )
-   | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
-       (* TASSI: da verificare *)
-       CicReduction.are_convertible ~subst ~metasenv context so ind ugraph
    | (_,_) -> false,ugraph
+ in
+  check_allowed_sort_elimination_aux ugraph context arity2 need_dummy
 	 
 and type_of_branch ~subst context argsno need_dummy outtype term constype =
  let module C = Cic in
@@ -1419,7 +1387,7 @@ and type_of_branch ~subst context argsno need_dummy outtype term constype =
        C.Prod (C.Anonymous,so,type_of_branch ~subst
         ((Some (name,(C.Decl so)))::context) argsno need_dummy
         (CicSubstitution.lift 1 outtype) term' de)
-  | _ -> raise (AssertFailure "20")
+  | _ -> raise (AssertFailure (lazy "20"))
 
 (* check_metasenv_consistency checks that the "canonical" context of a
 metavariable is consitent - up to relocation via the relocation list l -
@@ -1457,7 +1425,7 @@ and check_metasenv_consistency ~logger ~subst metasenv context
 	   if not b then
 	     raise 
 	       (TypeCheckerFailure 
-		  (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))
+		  (lazy (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t))))
 	   else
 	     ugraph1
        | Some t,Some (_,C.Decl ct) ->
@@ -1469,15 +1437,15 @@ and check_metasenv_consistency ~logger ~subst metasenv context
 	   in
            if not b then
              raise (TypeCheckerFailure 
-		      (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s" 
+		     (lazy (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s" 
 			 (CicPp.ppterm ct) (CicPp.ppterm t)
-			 (CicPp.ppterm type_t)))
+			 (CicPp.ppterm type_t))))
 	   else
 	     ugraph2
        | None, _  ->
            raise (TypeCheckerFailure
-		    ("Not well typed metavariable local context: "^
-		     "an hypothesis, that is not hidden, is not instantiated"))
+		   (lazy ("Not well typed metavariable local context: "^
+		     "an hypothesis, that is not hidden, is not instantiated")))
      ) ugraph l lifted_canonical_context 
      
 
@@ -1502,10 +1470,10 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
              debug_print (lazy "##### CASO DA INVESTIGARE E CAPIRE") ;
               type_of_aux ~logger context (S.lift n bo) ugraph
           | None -> raise 
-	      (TypeCheckerFailure "Reference to deleted hypothesis")
+	      (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
         with
         _ ->
-          raise (TypeCheckerFailure "unbound variable")
+          raise (TypeCheckerFailure (lazy "unbound variable"))
        )
     | C.Var (uri,exp_named_subst) ->
       incr fdebug ;
@@ -1540,7 +1508,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
          (C.Sort (C.Type t')),ugraph1
       (* TASSI: CONSTRAINTS *)
     | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
-    | C.Implicit _ -> raise (AssertFailure "21")
+    | C.Implicit _ -> raise (AssertFailure (lazy "21"))
     | C.Cast (te,ty) as t ->
        let _,ugraph1 = type_of_aux ~logger context ty ugraph in
        let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
@@ -1551,7 +1519,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
            ty,ugraph3
 	 else
            raise (TypeCheckerFailure
-		    (sprintf "Invalid cast %s" (CicPp.ppterm t)))
+		    (lazy (sprintf "Invalid cast %s" (CicPp.ppterm t))))
     | C.Prod (name,s,t) ->
        let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
        let sort2,ugraph2 = 
@@ -1565,9 +1533,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
          | C.Sort _ -> ()
          | _ ->
            raise
-            (TypeCheckerFailure (sprintf
+            (TypeCheckerFailure (lazy (sprintf
               "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s)
-                (CicPp.ppterm sort1)))
+                (CicPp.ppterm sort1))))
        ) ;
        let type2,ugraph2 = 
 	 type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1 
@@ -1606,7 +1574,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 	 (* TASSI: questa c'era nel mio... ma non nel CVS... *)
 	 (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *)
 	 eat_prods ~subst context hetype tlbody_and_type ugraph2
-   | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
+   | C.Appl _ -> raise (AssertFailure (lazy "Appl: no arguments"))
    | C.Const (uri,exp_named_subst) ->
        incr fdebug ;
        let ugraph1 = 
@@ -1668,9 +1636,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
             | _ ->
 		raise 
 		  (TypeCheckerFailure 
-		     (sprintf
+		     (lazy (sprintf
 			"Malformed case analasys' output type %s" 
-			(CicPp.ppterm outtype)))
+			(CicPp.ppterm outtype))))
       in
 (*
       let (parameters, arguments, exp_named_subst),ugraph2 =
@@ -1686,9 +1654,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 		else 
 		  raise 
 		    (TypeCheckerFailure 
-		       (sprintf
+		      (lazy (sprintf
 			  ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
-			  (CicPp.ppterm typ) (U.string_of_uri uri) i))
+			  (CicPp.ppterm typ) (U.string_of_uri uri) i)))
             | C.Appl 
 		((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
 		if U.eq uri uri' && i = i' then
@@ -1698,18 +1666,18 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 		else 
 		  raise 
 		    (TypeCheckerFailure 
-		       (sprintf 
+		      (lazy (sprintf 
 			  ("Case analysys: analysed term type is %s, "^
 			   "but is expected to be (an application of) "^
 			   "%s#1/%d{_}")
-			  (CicPp.ppterm typ') (U.string_of_uri uri) i))
+			  (CicPp.ppterm typ') (U.string_of_uri uri) i)))
             | _ ->
 		raise 
 		  (TypeCheckerFailure 
-		     (sprintf
+		    (lazy (sprintf
 			("Case analysis: "^
 			 "analysed term %s is not an inductive one")
-			(CicPp.ppterm term)))
+			(CicPp.ppterm term))))
 *)
       let (b, k) = guess_args context outsort in
 	  if not b then (b, k - 1) else (b, k) in
@@ -1721,26 +1689,25 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 		([],[],exp_named_subst),ugraph2
               else raise 
 		(TypeCheckerFailure 
-		   (sprintf
+		  (lazy (sprintf
 		      ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
-		      (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
-          | C.Appl 
-	      ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
+		      (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)))
+          | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) ->
               if U.eq uri uri' && i = i' then
 		let params,args =
 		  split tl (List.length tl - k)
 		in (params,args,exp_named_subst),ugraph2
               else raise 
 		(TypeCheckerFailure 
-		   (sprintf
+		  (lazy (sprintf
 		      ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
-		      (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
+		      (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)))
           | _ ->
               raise 
 		(TypeCheckerFailure 
-		   (sprintf
+		  (lazy (sprintf
 		      "Case analysis: analysed term %s is not an inductive one"
-                      (CicPp.ppterm term)))
+                      (CicPp.ppterm term))))
       in
 	(* 
 	   let's control if the sort elimination is allowed: 
@@ -1760,7 +1727,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
       in
 	if not b then
         raise
-          (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
+          (TypeCheckerFailure (lazy ("Case analasys: sort elimination not allowed")));
         (* let's check if the type of branches are right *)
       let parsno =
         let obj,_ =
@@ -1772,8 +1739,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
             C.InductiveDefinition (_,_,parsno,_) -> parsno
           | _ ->
               raise (TypeCheckerFailure
-                ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri))
+                (lazy ("Unknown mutual inductive definition:" ^
+                  UriManager.string_of_uri uri)))
 	in
       let (_,branches_ok,ugraph5) =
         List.fold_left
@@ -1807,7 +1774,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
          in
           if not branches_ok then
            raise
-            (TypeCheckerFailure "Case analysys: wrong branch type");
+            (TypeCheckerFailure (lazy "Case analysys: wrong branch type"));
           let arguments' =
            if not need_dummy then outtype::arguments@[term]
            else outtype::arguments in
@@ -1849,12 +1816,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 			       (len + eaten) kl 1 [] m) then
 		       raise
 			 (TypeCheckerFailure 
-			    ("Fix: not guarded by destructors"))
+			   (lazy ("Fix: not guarded by destructors")))
 		     else
 		       ugraph2
 		 end
                else
-		 raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
+		 raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies")))
           ) ugraph1 fl in
 	(*CSC: controlli mancanti solo su D{f,k,x,M} *)
       let (_,_,ty,_) = List.nth fl i in
@@ -1886,7 +1853,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 			None ->
 			  raise
 			  (TypeCheckerFailure
-			     ("CoFix: does not return a coinductive type"))
+			    (lazy "CoFix: does not return a coinductive type"))
 		      | Some uri ->
 			  (*
 			    let's control the guarded by constructors 
@@ -1896,13 +1863,13 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
                               (types @ context) 0 len false bo [] uri) then
 			    raise
 			      (TypeCheckerFailure 
-				 ("CoFix: not guarded by constructors"))
+				(lazy "CoFix: not guarded by constructors"))
 			  else
 			  ugraph2
 		  end
 		else
 		  raise
-		    (TypeCheckerFailure ("CoFix: ill-typed bodies"))
+		    (TypeCheckerFailure (lazy "CoFix: ill-typed bodies"))
            ) ugraph1 fl 
        in
        let (_,ty,_) = List.nth fl i in
@@ -1931,7 +1898,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 		      ~subst ~metasenv context typeoft typeofvar ugraph2) ;
 		 fdebug := 0 ;
 		 debug typeoft [typeofvar] ;
-		 raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
+		 raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution"))
                end
    in
      check_exp_named_subst_aux ~logger [] ugraph 
@@ -1958,9 +1925,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
     | (C.Meta _, (C.Meta (_,_) as t))
     | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
         t2',ugraph
-    | (_,_) -> raise (TypeCheckerFailure (sprintf
+    | (_,_) -> raise (TypeCheckerFailure (lazy (sprintf
         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
-          (CicPp.ppterm t2')))
+          (CicPp.ppterm t2'))))
 
  and eat_prods ~subst context hetype l ugraph =
    (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
@@ -1990,13 +1957,13 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
 		      debug s [hety] ;
 		      raise 
 			(TypeCheckerFailure 
-			   (sprintf
+			  (lazy (sprintf
 			      ("Appl: wrong parameter-type, expected %s, found %s")
-			      (CicPp.ppterm hetype) (CicPp.ppterm s)))
+			      (CicPp.ppterm hetype) (CicPp.ppterm s))))
 		    end
 	    | _ ->
 		raise (TypeCheckerFailure
-			 "Appl: this is not a function, it cannot be applied")
+			(lazy "Appl: this is not a function, it cannot be applied"))
 	 )
 
  and returns_a_coinductive ~subst context ty =
@@ -2015,8 +1982,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
              if is_inductive then None else (Some uri)
          | _ ->
             raise (TypeCheckerFailure
-              ("Unknown mutual inductive definition:" ^
-              UriManager.string_of_uri uri))
+              (lazy ("Unknown mutual inductive definition:" ^
+              UriManager.string_of_uri uri)))
         )
     | C.Appl ((C.MutInd (uri,i,_))::_) ->
        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
@@ -2026,8 +1993,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
              if is_inductive then None else (Some uri)
          | _ ->
             raise (TypeCheckerFailure
-              ("Unknown mutual inductive definition:" ^
-              UriManager.string_of_uri uri))
+              (lazy ("Unknown mutual inductive definition:" ^
+              UriManager.string_of_uri uri)))
         )
     | C.Prod (n,so,de) ->
        returns_a_coinductive ~subst ((Some (n,C.Decl so))::context) de
@@ -2045,21 +2012,32 @@ in debug_print (lazy "FINE TYPE_OF_AUX") ; flush stderr ; res
 
 (* is a small constructor? *)
 (*CSC: ottimizzare calcolando staticamente *)
-and is_small ~logger context paramsno c ugraph =
- let rec is_small_aux ~logger context c ugraph =
+and is_small_or_non_informative ~condition ~logger context paramsno c ugraph =
+ let rec is_small_or_non_informative_aux ~logger context c ugraph =
   let module C = Cic in
    match CicReduction.whd context c with
       C.Prod (n,so,de) ->
        let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in
-       let b = (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) in
+       let b = condition s in
        if b then
-         is_small_aux ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
+         is_small_or_non_informative_aux
+          ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
        else 
        	 false,ugraph1
     | _ -> true,ugraph (*CSC: we trust the type-checker *)
  in
   let (context',dx) = split_prods ~subst:[] context paramsno c in
-   is_small_aux ~logger context' dx ugraph
+   is_small_or_non_informative_aux ~logger context' dx ugraph
+
+and is_small ~logger =
+ is_small_or_non_informative
+  ~condition:(fun s -> s=Cic.Sort Cic.Prop || s=Cic.Sort Cic.Set)
+  ~logger
+
+and is_non_informative ~logger =
+ is_small_or_non_informative
+  ~condition:(fun s -> s=Cic.Sort Cic.Prop)
+  ~logger
 
 and type_of ~logger t ugraph =
 (*CSC
@@ -2081,7 +2059,10 @@ let typecheck_obj0 ~logger uri ugraph =
       let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
        if not b then
          raise (TypeCheckerFailure
-          ("the type of the body is not the one expected"))
+          (lazy
+            ("the type of the body is not the one expected:\n" ^
+             CicPp.ppterm ty_te ^ "\nvs\n" ^
+             CicPp.ppterm ty)))
        else
         ugraph
    | C.Constant (_,None,ty,_,_) ->
@@ -2104,9 +2085,9 @@ let typecheck_obj0 ~logger uri ugraph =
        in
        let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
         if not b then
-          raise (TypeCheckerFailure (sprintf
+          raise (TypeCheckerFailure (lazy (sprintf
            "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
-           (CicPp.ppterm type_of_te) (CicPp.ppterm ty)))
+           (CicPp.ppterm type_of_te) (CicPp.ppterm ty))))
         else
          ugraph
    | C.Variable (_,bo,ty,_,_) ->
@@ -2119,7 +2100,7 @@ let typecheck_obj0 ~logger uri ugraph =
   	    let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
              if not b then
               raise (TypeCheckerFailure
-               ("the body is not the one expected"))
+               (lazy "the body is not the one expected"))
              else
               ugraph
             )
@@ -2174,3 +2155,16 @@ let typecheck_obj uri obj =
  let logger = new CicLogger.logger in
  typecheck_obj ~logger uri obj
 
+(* check_allowed_sort_elimination uri i s1 s2
+   This function is used outside the kernel to determine in advance whether
+   a MutCase will be allowed or not.
+   [uri,i] is the type of the term to match
+   [s1] is the sort of the term to eliminate (i.e. the head of the arity
+        of the inductive type [uri,i])
+   [s2] is the sort of the goal (i.e. the head of the type of the outtype
+        of the MutCase) *)
+let check_allowed_sort_elimination uri i s1 s2 =
+ fst (check_allowed_sort_elimination ~subst:[] ~metasenv:[]
+  ~logger:(new CicLogger.logger) [] uri i true
+  (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2)
+  CicUniv.empty_ugraph)