prima implementazione di demodulate, superposition_left e superposition_right

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 74542a22696ce39cac7d3d9e81f63acf67a6817c..fbcf25f91450a4beb8ace412ba213dcfc0fa0d6c 100644 (file)
--- 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