diff options
| author |  Gregory Malecha <gmalecha@cs.harvard.edu> | 2014-05-10 00:47:16 -0400 |
|---|---|---|
| committer |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-05-26 13:37:36 +0200 |
| commit | 13deafee96893a5ec332ad221469e3e5460693f1 (patch) | |
| tree | c33a858cee5305f75b5d67f24724e7aa2e085a87 /kernel/constr.mli | |
| parent | 525094414bf74445f930e170a823a49107726f6f (diff) | |
make coqdep canonicalize paths from the command line
- logical paths given to -R and -I should be split
on periods.
- it also seems like giving an empty string should
result in the empty path rather than the singleton
path with an empty string as an identifier.
Diffstat (limited to 'kernel/constr.mli')
0 files changed, 0 insertions, 0 deletions