diff options
| author | Pierre Boutillier | 2014-06-30 14:00:39 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-06-30 15:55:54 +0200 |
| commit | e1d46f1c6ca9556e23e5378c6589220fc48da879 (patch) | |
| tree | 6000c8c03de02115f134864dbbf64b0922cf2a7b /kernel/nativelambda.mli | |
| parent | 8e3ef4dbfd00c67af1cc2b83307038a6440584cb (diff) | |
Coqdep: update include strategies
-I is (only) the ml one
-I -as is fixed
-Q is understood
-R is not a recursive ml include anymore
$COQENV, user_contrib, ... are not recursively included
coqlib/theories and coqlib/plugins are still recursively included (for now). (This
may deserves an option)
Closes Bug 2910: If there is a "Require a." in a b.v and a a.vo in path but no a.v,
coqdep does not complains about a missing a.v.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions