- R.are_convertible context (type_of_aux' metasenv context t) ct
- | _, _ -> false
- in
- if not res then raise (TypeCheckerFailure MetasenvInconsistency)
+ let type_t = type_of_aux' metasenv context t in
+ if not (R.are_convertible context type_t ct) then
+ raise (TypeCheckerFailure (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)))
+ | None, _ ->
+ raise (TypeCheckerFailure
+ "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated")