diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-29 11:59:17 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-29 11:59:17 +0000 |
commit | 5625678dcc3e35fb2799a0a9d1fd8d3daa764db3 (patch) | |
tree | d362542a6ef54261009e4bbec9f722e9ee6c7f87 /library/heads.ml | |
parent | 5893703b77fb17885fd66dbf575b9533cbf96a90 (diff) |
Added Add LoadPath in coqdep lexer (but not in coqdep itself by lack of time).
There are preliminary problems to solve in the semantics of -I/-R which
differs from the one of coqtop:
- in case of ambiguity, internally to -R option, or between two -R/-I options,
it is not clear at all that the semantics is as in coqtop (which by the way
is not canonical either since it seems to depend on the underlying order of
dirs in the file system),
- in the presence of -I dir, Require A.b does not look if dir.A.b exists;
similarly for Declare ML Module "f", Require "f" and Load "f" when f has
a dirname part.
I suggest to have a common library for coqdep, coqdoc and coqtop that
ensures that -I/-R behave consistently for all tools.
Incidentally made coqdep lexer a bit more strict about syntax errors.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14626 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/heads.ml')
0 files changed, 0 insertions, 0 deletions