aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/heads.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-10-29 11:59:17 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-10-29 11:59:17 +0000
commit5625678dcc3e35fb2799a0a9d1fd8d3daa764db3 (patch)
treed362542a6ef54261009e4bbec9f722e9ee6c7f87 /library/heads.ml
parent5893703b77fb17885fd66dbf575b9533cbf96a90 (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