diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-22 10:01:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-31 00:52:26 +0200 |
| commit | d9ea37641bc67ca269065a9489ec8e70b2f2d246 (patch) | |
| tree | d4c7c232abc82c84994979e68a518c692abd3635 /interp | |
| parent | ca630605330828b9b6456477b0fd4f8a0c3f1831 (diff) | |
Locating error about clash between a inductive parameter and a bound variable.
Also trying to reformulate the message, distinguishing between a
variable/parameter and its name.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ce51f21c7..6f01f6a50 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -361,13 +361,14 @@ let reset_hidden_inductive_implicit_test env = | (Inductive (params,_),b,c,d) -> (Inductive (params,false),b,c,d) | x -> x) env.impls } -let check_hidden_implicit_parameters id impls = +let check_hidden_implicit_parameters ?loc id impls = if Id.Map.exists (fun _ -> function | (Inductive (indparams,check),_,_,_) when check -> Id.List.mem id indparams | _ -> false) impls then - user_err (strbrk "A parameter of an inductive type " ++ - pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") + user_err ?loc (pr_id id ++ strbrk " is already used as name of " ++ + strbrk "a parameter of the inductive type; bound variables in " ++ + strbrk "the type of a constructor shall use a different name.") let push_name_env ?(global_level=false) ntnvars implargs env = function @@ -376,7 +377,7 @@ let push_name_env ?(global_level=false) ntnvars implargs env = user_err ?loc (str "Anonymous variables not allowed"); env | loc,Name id -> - check_hidden_implicit_parameters id env.impls ; + check_hidden_implicit_parameters ?loc id env.impls ; if Id.Map.is_empty ntnvars && Id.equal id ldots_var then error_ldots_var ?loc; set_var_scope ?loc id false env ntnvars; |