| CicMetaSubst.MetaSubstFailure msg ->
raise (AssertFailure
((sprintf
- "Type checking error: %s in context\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
+ "Type checking error: %s in context\n%s\nand metasenv\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
(CicMetaSubst.ppterm subst term)
- (CicMetaSubst.ppcontext subst context) msg)))
+ (CicMetaSubst.ppcontext subst context)
+ (CicMetaSubst.ppmetasenv metasenv subst) msg)))
(* NUOVA UNIFICAZIONE *)
(* A substitution is a (int * Cic.term) list that associates a
else
raise (UnificationFailure (sprintf
"Can't unify %s with %s due to different constants"
- (CicPp.ppterm t1) (CicPp.ppterm t1)))
+ (CicPp.ppterm t1) (CicPp.ppterm t2)))
| C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
if UriManager.eq uri1 uri2 && i1 = i2 then
fo_unif_subst_exp_named_subst subst context metasenv