diff options
| author | Pierre-Marie Pédrot | 2020-07-22 12:52:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-22 12:52:36 +0200 |
| commit | 3962027eece19261efe88dda6c5a655f99ae93d0 (patch) | |
| tree | 76b7d4f231f7a1af0640828fc2610ca0accc540f /vernac/comPrimitive.ml | |
| parent | 56fd98a932f2700a63fe701bb71533fb48d6d06b (diff) | |
| parent | 7461fe4f55ad9ee7c55c9b060e74a49d173b4ce7 (diff) | |
Merge PR #12664: Turn various anomalies into regular errors in primitive declaration path
Reviewed-by: ppedrot
Diffstat (limited to 'vernac/comPrimitive.ml')
| -rw-r--r-- | vernac/comPrimitive.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml index 110dcdc98a..eaa5271a73 100644 --- a/vernac/comPrimitive.ml +++ b/vernac/comPrimitive.ml @@ -38,7 +38,13 @@ let do_primitive id udecl prim typopt = Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env) env evd typ in - let evd = Evarconv.unify_delay env evd typ expected_typ in + let evd = try Evarconv.unify_delay env evd typ expected_typ + with Evarconv.UnableToUnify (evd,e) as exn -> + let _, info = Exninfo.capture exn in + Exninfo.iraise (Pretype_errors.( + PretypeError (env,evd,CannotUnify (typ,expected_typ,Some e)),info)) + in + Pretyping.check_evars_are_solved ~program_mode:false env evd; let evd = Evd.minimize_universes evd in let uvars = EConstr.universes_of_constr evd typ in let evd = Evd.restrict_universe_context evd uvars in |