]> matita.cs.unibo.it Git - helm.git/commit
bugfix to developments:
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 5 Jul 2006 10:40:11 +0000 (10:40 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 5 Jul 2006 10:40:11 +0000 (10:40 +0000)
commit81b53ddc3ce92187e62deff483919ca2251fd246
treecc4ce207f17514743e78b009dcf130d3a469bc3e
parent227ed314d21d52a2270073bf534eae452732a791
bugfix to developments:
- if an included .ma file is not found (not in CWD, not in include_paths)
  an error is issued
- if an included .ma file is found but the corrsponding .lexicon is not found
  a development for the .ma is searched:
  - if found it is used to compile the .ma file
  - if not found the user is aked to create a devel for the file included
    (and not the file that he is editing, that may not be in the same devel).
13 files changed:
components/grafite_engine/grafiteEngine.ml
components/grafite_engine/grafiteEngine.mli
components/grafite_parser/dependenciesParser.ml
components/grafite_parser/dependenciesParser.mli
components/grafite_parser/grafiteParser.ml
components/lexicon/lexiconAst.ml
components/lexicon/lexiconAstPp.ml
components/lexicon/lexiconEngine.ml
components/lexicon/lexiconEngine.mli
matita/matitaScript.ml
matita/matitacLib.ml
matita/matitaclean.ml
matita/matitadep.ml