diff options
| author |  Julien Forest <julien.forest@ensiie.fr> | 2018-04-09 21:28:24 +0200 |
|---|---|---|
| committer | Julien Forest <julien.forest@ensiie.fr> | 2018-04-09 21:28:24 +0200 |
| commit | 577738531f607da8e6347ade1dc3767d98aaf863 (patch) | |
| tree | 025d51c19c016dbe31e6104131088770e14de888 /plugins/funind | |
| parent | ce3c7ee7cadcab9a194fb37e0d500948078acda0 (diff) | |
change error message in #5147
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index b3f08301b..804548ce5 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -633,7 +633,7 @@ let build_scheme fas = let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in if isConst f then (destConst f,sort) - else user_err Pp.(pr_constr_env (Global.env ()) !evd f ++spc () ++ str "should be a function") + else user_err Pp.(pr_constr_env (Global.env ()) !evd f ++spc () ++ str "should be the named of a globally defined function") ) fas ) in |