diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-04-05 13:14:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-04-05 13:29:08 +0200 |
| commit | 8c3455e2f5db09e70cd7a40a96856f5be79adaff (patch) | |
| tree | 11a3374e1a50ba451c40676178a86fd1c619bc52 | |
| parent | ea1e45096184bdb963b3572733654d1a15617bdd (diff) | |
Fixing bug #3228 (fixing precedence of ltac variables over variables in env).
| -rw-r--r-- | pretyping/pretyping.ml | 10 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3228.v | 7 |
2 files changed, 12 insertions, 5 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index def8dbfb1..c66221e5f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -249,16 +249,16 @@ let pretype_id loc env sigma (lvar,unbndltacvars) id = let c = substl subst c in { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> + (* Check if [id] is a ltac variable not bound to a term *) + (* and build a nice error message *) + if Id.Map.mem id unbndltacvars then + user_err_loc (loc,"", + str "Variable " ++ pr_id id ++ str " should be bound to a term."); (* Check if [id] is a section or goal variable *) try let (_,_,typ) = lookup_named id env in { uj_val = mkVar id; uj_type = typ } with Not_found -> - (* [id] not found, build nice error message if [id] yet known from ltac *) - if Id.Map.mem id unbndltacvars then - user_err_loc (loc,"", - str "Variable " ++ pr_id id ++ str " should be bound to a term.") - else (* [id] not found, standard error message *) error_var_not_found_loc loc id diff --git a/test-suite/bugs/closed/3228.v b/test-suite/bugs/closed/3228.v new file mode 100644 index 000000000..5d1a0ff88 --- /dev/null +++ b/test-suite/bugs/closed/3228.v @@ -0,0 +1,7 @@ +(* Check that variables in the context do not take precedence over + ltac variables *) + +Ltac bar x := exact x. +Goal False -> False. + intro x. + Fail bar doesnotexist. |