From 3fe4912b568916676644baeb982a3e10c592d887 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 25 Sep 2014 00:12:26 +0200 Subject: Keyed unification option, compiling the whole standard library (but deactivated still). Set Keyed Unification to activate the option, which changes subterm selection to _always_ use full conversion _after_ finding a subterm whose head/key matches the key of the term we're looking for. This applies to rewrite and higher-order unification in apply/elim/destruct. Most proof scripts already abide by these semantics. For those that don't, it's usually only a matter of using: Declare Equivalent Keys f g. This make keyed unification consider f and g to match as keys. This takes care of most cases of abbreviations: typically Def foo := bar and rewriting with a bar-headed lhs in a goal mentioning foo works once they're set equivalent. For canonical structures, these hints should be automatically declared. For non-global-reference headed terms, the key is the constructor name (Sort, Prod...). Evars and metas are no keys. INCOMPATIBILITIES: In FMapFullAVL, a Function definition doesn't go through with keyed unification on. --- library/keys.mli | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'library/keys.mli') diff --git a/library/keys.mli b/library/keys.mli index 87ba45558..36789c83b 100644 --- a/library/keys.mli +++ b/library/keys.mli @@ -10,11 +10,14 @@ open Globnames type key -val declare_keys : key -> key -> unit +val declare_equiv_keys : key -> key -> unit (** Declare two keys as being equivalent. *) val equiv_keys : key -> key -> bool (** Check equivalence of keys. *) -val constr_key : Term.constr -> key +val constr_key : Term.constr -> key option (** Compute the head key of a term. *) + +val pr_keys : (global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds +(** Pretty-print the mapping *) -- cgit v1.2.3