diff options
| author | Pierre-Marie Pédrot | 2020-10-15 15:14:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-15 15:14:23 +0200 |
| commit | 4bf43453ec5f635ae87a2edeb4f51d95f2d5ac67 (patch) | |
| tree | ce78494f5923cdde51c7a3ba4acf0133b1640bfe /vernac | |
| parent | fc0ee016b2bbffd73c5a9aa7784f2c255f80d39d (diff) | |
| parent | 34e1aeef7718dd3042ef22cd1ded9d9eb65cfd87 (diff) | |
Merge PR #13181: Guard unify_leq_delay calls in Typing
Reviewed-by: ppedrot
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a9de01bfd0..5f7eb78a40 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -866,7 +866,7 @@ let explain_unsatisfiable_constraints env sigma constr comp = let info = Evar.Map.find ev undef in explain_typeclass_resolution env sigma info k ++ fnl () ++ cstr -let explain_pretype_error env sigma err = +let rec explain_pretype_error env sigma err = let env = Evardefine.env_nf_betaiotaevar sigma env in let env = make_all_name_different env sigma in match err with @@ -893,7 +893,7 @@ let explain_pretype_error env sigma err = | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env sigma m n | CannotFindWellTypedAbstraction (p,l,e) -> explain_cannot_find_well_typed_abstraction env sigma p l - (Option.map (fun (env',e) -> explain_type_error env' sigma e) e) + (Option.map (fun (env',e) -> explain_pretype_error env' sigma e) e) | WrongAbstractionType (n,a,t,u) -> explain_wrong_abstraction_type env sigma n a t u | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n |