X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=fbcf25f91450a4beb8ace412ba213dcfc0fa0d6c;hb=349a0e23813a7f33853e1f8fe48230276ac22934;hp=74542a22696ce39cac7d3d9e81f63acf67a6817c;hpb=46f19eadce5f3a11c0ae26934fd8d1b597906416;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 74542a226..fbcf25f91 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -903,7 +903,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
        (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
        exp_named_subst true
    | C.MutCase (uri,i,outtype,term,pl) ->
-      (match term with
+      (match CicReduction.whd context term with
           C.Rel m when List.mem m safes || m = x ->
            let (tys,len,isinductive,paramsno,cl) =
 	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
@@ -1680,8 +1680,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
               else raise 
 		(TypeCheckerFailure 
 		   (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))
+		      ("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' ->
               if U.eq uri uri' && i = i' then
@@ -1691,8 +1691,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
               else raise 
 		(TypeCheckerFailure 
 		   (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))
+		      ("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))
           | _ ->
               raise 
 		(TypeCheckerFailure