diff options
| author | Matthieu Sozeau | 2015-01-14 18:05:40 +0530 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-15 18:59:00 +0530 |
| commit | 004b7f53cd9a9f8bd78156310f516af8fe42554b (patch) | |
| tree | b207cc0bcec74dbdf362850464e35d95d7d467ea /tactics | |
| parent | 6965121294e2a083c0111d6ff3da2158ed6f4a7a (diff) | |
Optionally allow eta-conversion during unification for type classes.
Off by default as it can be backwards-incompatible (e.g. produces
loop in the library without an additional Typeclasses Opaque directive
in RelationPairs).
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 44204a9f0e..9d49a7bbb7 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -32,6 +32,21 @@ open Hints let typeclasses_debug = ref false let typeclasses_depth = ref None +let typeclasses_modulo_eta = ref false +let set_typeclasses_modulo_eta d = (:=) typeclasses_modulo_eta d +let get_typeclasses_modulo_eta () = !typeclasses_modulo_eta + +open Goptions + +let set_typeclasses_modulo_eta = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "do typeclass search modulo eta conversion"; + optkey = ["Typeclasses";"Modulo";"Eta"]; + optread = get_typeclasses_modulo_eta; + optwrite = set_typeclasses_modulo_eta; } + (** We transform the evars that are concerned by this resolution (according to predicate p) into goals. Invariant: function p only manipulates and returns undefined evars *) @@ -65,7 +80,7 @@ let auto_core_unif_flags st freeze = { frozen_evars = freeze; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = true; - modulo_eta = false; + modulo_eta = !typeclasses_modulo_eta; } let auto_unif_flags freeze st = |