diff options
| author | Matthieu Sozeau | 2015-01-14 18:05:40 +0530 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-18 00:16:42 +0530 |
| commit | ed339b1eef52a73e6e170b2613e65c1037105132 (patch) | |
| tree | fba722b85f6cde8c738e46e754b13879efdc677a /tactics | |
| parent | f9a3a366a6abc53c5d8bc8a7adf3a102b49afecc (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 = |