diff options
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/GlobalSettings.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Util/GlobalSettings.v b/src/Util/GlobalSettings.v index f8ab4964f..799290e1b 100644 --- a/src/Util/GlobalSettings.v +++ b/src/Util/GlobalSettings.v @@ -25,3 +25,6 @@ Global Set Uniform Inductive Parameters. (** Better-behaved [simpl] *) (** Set SimplIsCbn. *) + +(** Faster printing *) +Global Set Fast Name Printing. |