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.

1 files changed, 16 insertions, 0 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0647fa8130..ffd164d16a 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -994,3 +994,19 @@ let decompose l c =
 TACTIC EXTEND decompose
 | [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ]
 END
+
+(** library/keys *)
+
+VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
+| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [ 
+  let it c = snd (Constrintern.interp_open_constr (Global.env ()) Evd.empty c) in 
+  let k1 = Keys.constr_key (it c) in
+  let k2 = Keys.constr_key (it c') in
+    match k1, k2 with
+    | Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2
+    | _ -> () ]
+END
+
+VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY
+| [ "Print" "Equivalent" "Keys" ] -> [ msg_info (Keys.pr_keys Printer.pr_global) ]
+END