diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-14 18:05:40 +0530 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-15 18:59:00 +0530 |
| commit | 004b7f53cd9a9f8bd78156310f516af8fe42554b (patch) | |
| tree | b207cc0bcec74dbdf362850464e35d95d7d467ea | |
| 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).
| -rw-r--r-- | tactics/class_tactics.ml | 17 | ||||
| -rw-r--r-- | theories/Classes/RelationPairs.v | 1 |
2 files changed, 17 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 44204a9f0..9d49a7bbb 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 = diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index cbde5f9ab..8ce3e4b6b 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -42,6 +42,7 @@ Generalizable Variables A B RA RB Ri Ro f. Definition RelCompFun {A} {B : Type}(R:relation B)(f:A->B) : relation A := fun a a' => R (f a) (f a'). +Typeclasses Opaque RelCompFun. Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope. |