diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-11-29 14:37:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-11-29 14:37:37 +0100 |
| commit | 46c3ab137fe6705293e8a44624e2a564cde1d55a (patch) | |
| tree | 21c2e9b70139e98ba71ea2705bc5e1dd0ad86d9b /checker | |
| parent | bbe7b785787ff3f13e5c2809a67241981b06e1db (diff) | |
Add a -Q option to coqchck.
It has exactly the same effect as -R, because there is no such thing as
implicit relativization for object files in coqchk, contrarily to what
Require does in coqtop.
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/checker.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index b2433ee36..cc285d5e4 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -329,6 +329,9 @@ let parse_args argv = | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () + | "-Q" :: d :: p :: rem -> set_rec_include d p;parse rem + | "-Q" :: ([] | [_]) -> usage () + | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem | "-R" :: ([] | [_]) -> usage () |