diff options
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/library/lib.ml b/library/lib.ml index c27c9c04c5..16521e627b 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -105,6 +105,10 @@ let make_kn id = let mp,dir = current_prefix () in Names.make_kn mp dir (label_of_id id) +let make_con id = + let mp,dir = current_prefix () in + Names.make_con mp dir (label_of_id id) + let make_oname id = make_path id, make_kn id |