diff options
| -rw-r--r-- | library/keys.ml | 4 | ||||
| -rw-r--r-- | library/keys.mli | 2 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 12 | ||||
| -rw-r--r-- | pretyping/unification.ml | 4 |
4 files changed, 13 insertions, 9 deletions
diff --git a/library/keys.ml b/library/keys.ml index 057dc3b65..c9e325ee5 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -114,11 +114,11 @@ let inKeys : key_obj -> obj = let declare_equiv_keys ref ref' = Lib.add_anonymous_leaf (inKeys (ref,ref')) -let constr_key c = +let constr_key kind c = let open Globnames in try let rec aux k = - match kind_of_term k with + match kind k with | Const (c, _) -> KGlob (ConstRef c) | Ind (i, u) -> KGlob (IndRef i) | Construct (c,u) -> KGlob (ConstructRef c) diff --git a/library/keys.mli b/library/keys.mli index 69668590d..6abac4de4 100644 --- a/library/keys.mli +++ b/library/keys.mli @@ -16,7 +16,7 @@ val declare_equiv_keys : key -> key -> unit val equiv_keys : key -> key -> bool (** Check equivalence of keys. *) -val constr_key : Term.constr -> key option +val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option (** Compute the head key of a term. *) val pr_keys : (global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index b34afd51b..1ec52718a 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -1087,10 +1087,14 @@ END (** library/keys *) VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF -| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [ - let it c = EConstr.Unsafe.to_constr (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 +| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [ + let get_key c = + let (evd, c) = Constrintern.interp_open_constr (Global.env ()) Evd.empty c in + let kind c = EConstr.kind evd c in + Keys.constr_key kind c + in + let k1 = get_key c in + let k2 = get_key c' in match k1, k2 with | Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2 | _ -> () ] diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 91781a076..eb90dfbdb 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1739,7 +1739,7 @@ let keyed_unify env evd kop = | None -> fun _ -> true | Some kop -> fun cl -> - let kc = Keys.constr_key (EConstr.to_constr evd cl) in + let kc = Keys.constr_key (fun c -> EConstr.kind evd c) cl in match kc with | None -> false | Some kc -> Keys.equiv_keys kop kc @@ -1749,7 +1749,7 @@ let keyed_unify env evd kop = Fails if no match is found *) let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = let bestexn = ref None in - let kop = Keys.constr_key (EConstr.to_constr evd op) in + let kop = Keys.constr_key (fun c -> EConstr.kind evd c) op in let rec matchrec cl = let cl = strip_outer_cast evd cl in (try |