blob: 001799aa31a5a65ace3e7af6b4c6ca75848055f1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
(** * Global Settings across the project *)
(** Compatibility with 8.4 so we can write, e.g., [match p with
ex_intro x y => _ end], rather than [match p with ex_intro _ x y
=> _ end]. *)
Global Set Asymmetric Patterns.
(** Consider also: *)
(** Judgmental η for records, faster projections *)
(** Set Primitive Projections. *)
(** Don't use non-imported hints *)
(** Set Loose Hint Behavior "Strict". *)
(** Universes *)
(** Set Universe Polymorphism. *)
(** Set Strict Universe Declaration. *)
(** Unset Universe Minimization ToSet. *)
(** Better control of unfolding in [rewrite] and [setoid_rewrite] *)
(** Set Keyed Unification. *)
(** Better-behaved [simpl] *)
(** Set SimplIsCbn. *)
|
