diff options
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index d3a602ac28..f1f95695d3 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -53,7 +53,7 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} = {utj_val=type_app (nf_evar sigma) v;utj_type=t} let env_ise sigma env = - let sign = named_context env in + let sign = named_context_val env in let ctxt = rel_context env in let env0 = reset_with_named_context sign env in Sign.fold_rel_context |