diff options
| author | Matej Košík | 2017-05-29 11:02:06 +0200 |
|---|---|---|
| committer | Matej Košík | 2017-06-10 10:33:53 +0200 |
| commit | b6feaafc7602917a8ef86fb8adc9651ff765e710 (patch) | |
| tree | 5a033488c31040009adb725f20e8bd0a5dd31bc5 /plugins/funind/merge.ml | |
| parent | 102d7418e399de646b069924277e4baea1badaca (diff) | |
Remove (useless) aliases from the API.
Diffstat (limited to 'plugins/funind/merge.ml')
| -rw-r--r-- | plugins/funind/merge.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 290d0bb918..c75f7f868c 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -893,7 +893,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info = locate_constant f_ref in try find_Function_infos (kn_of_id id) with Not_found -> - user_err ~hdr:"indfun" (Nameops.pr_id id ++ str " has no functional scheme") + user_err ~hdr:"indfun" (Id.print id ++ str " has no functional scheme") (** [merge id1 id2 args1 args2 id] builds and declares a new inductive type called [id], representing the merged graphs of both graphs |