diff options
| author | Enrico Tassi | 2014-07-10 15:59:44 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-07-11 10:15:06 +0200 |
| commit | 2a805fd99b96746dbfe381d64cd7eaba84fdca79 (patch) | |
| tree | 77e0c47e097c4edebe9eea5f839488c91264e9b3 /toplevel | |
| parent | 31b99c5671c956de455372e43f935e1c70006f9d (diff) | |
Feedback: LoadedFile + Goals
LoadedFile is generated when a .vo is loaded
Goals is generated when -feedback-goals
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0ccb6faafd..be63db391d 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -360,6 +360,7 @@ let parse_args arglist = |"-compile-verbose" -> add_compile true (next ()) |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true |"-feedback-glob" -> Dumpglob.feedback_glob () + |"-feedback-goals" -> Flags.feedback_goals := true |"-exclude-dir" -> exclude_search_in_dirname (next ()) |"-init-file" -> set_rcfile (next ()) |"-inputstate"|"-is" -> set_inputstate (next ()) |