diff options
| author | Matthieu Sozeau | 2014-09-18 21:39:03 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-18 21:39:03 +0200 |
| commit | 23041481ff368b0b4cfc9a2493c9f465df90ea90 (patch) | |
| tree | fa981847c7fe17b18d4453403d19df9e32b26a38 /lib | |
| parent | dbdff037af1a80d223be6e4d093417bae301c583 (diff) | |
Fix debug printing with primitive projections.
Add a flag to indicate if we're in the toplevel or debuggger to not try
to retype terms in the wrong environment (and making find_rectype,
get_type_of untraceable). This fixes bug #3638 along with the previous
commit.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/flags.ml | 2 | ||||
| -rw-r--r-- | lib/flags.mli | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 0356863aba..a744ce9b0b 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -73,6 +73,8 @@ let async_proofs_is_master () = !async_proofs_mode = APon && !async_proofs_worker_id = "master" let debug = ref false +let in_debugger = ref false +let in_toplevel = ref false let profile = false diff --git a/lib/flags.mli b/lib/flags.mli index f94d80ffc4..e53de166d4 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -34,6 +34,8 @@ val string_of_priority : priority -> string val priority_of_string : string -> priority val debug : bool ref +val in_debugger : bool ref +val in_toplevel : bool ref val profile : bool |