From a95210435f336d89f44052170a7c65563e6e35f2 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 24 Sep 2014 22:19:46 +0200 Subject: Index keys instead of simply global references. --- library/keys.mli | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'library/keys.mli') diff --git a/library/keys.mli b/library/keys.mli index 4e6a803e4..87ba45558 100644 --- a/library/keys.mli +++ b/library/keys.mli @@ -8,8 +8,13 @@ open Globnames -val declare_keys : global_reference -> global_reference -> unit +type key + +val declare_keys : key -> key -> unit (** Declare two keys as being equivalent. *) -val equiv_keys : global_reference -> global_reference -> bool +val equiv_keys : key -> key -> bool (** Check equivalence of keys. *) + +val constr_key : Term.constr -> key +(** Compute the head key of a term. *) -- cgit v1.2.3