diff options
| author | Gaëtan Gilbert | 2019-02-08 16:10:46 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-11 12:56:07 +0100 |
| commit | ac7169182a970c33be2e33abd43be5bf19542e2c (patch) | |
| tree | 8c65962bb142c6bbbed1ff9354e63124174ba5a8 /pretyping/coercion.ml | |
| parent | 3352a5b7c4507ff8fda1f5aeba83f2e141cb7a3e (diff) | |
Fix #9527: unknown evar in nonterminating [fix] error.
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 9e93c470b1..2329b87acc 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -434,7 +434,7 @@ let inh_tosort_force ?loc env evd j = try let t,p = lookup_path_to_sort_from env evd j.uj_type in let evd,j1 = apply_coercion env evd p j t in - let j2 = on_judgment_type (whd_evar evd) j1 in + let j2 = Environ.on_judgment_type (whd_evar evd) j1 in (evd,type_judgment env evd j2) with Not_found | NoCoercion -> error_not_a_type ?loc env evd j |