diff options
| author | Maxime Dénès | 2018-10-30 11:03:26 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-30 13:10:02 +0100 |
| commit | 6214079b980b8a02bef20d5b25abbe49c3095f32 (patch) | |
| tree | 7f50070252445fa2147f81c7d0aeb65158e1ac0d /plugins | |
| parent | 0ac673e562c34245e4e48efc428d808e917be79b (diff) | |
Distinguish globalization and pretyping error on unbound variable
We can then avoid passing an empty env.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacintern.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 55412c74bb..a2b4156f50 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -83,7 +83,8 @@ let intern_hyp ist ({loc;v=id} as locid) = else if find_ident id ist then make id else - Pretype_errors.error_var_not_found ?loc id + CErrors.user_err ?loc Pp.(str "Hypothesis" ++ spc () ++ Id.print id ++ spc() ++ + str "was not found in the current environment.") let intern_or_var f ist = function | ArgVar locid -> ArgVar (intern_hyp ist locid) |