diff options
| author | letouzey | 2013-02-19 16:55:18 +0000 |
|---|---|---|
| committer | letouzey | 2013-02-19 16:55:18 +0000 |
| commit | ef64634b31a4cd999cd08636adbf117f81889fb1 (patch) | |
| tree | a8c4cf15e41961d90317dd1b97adfd70c39b67b2 /kernel/names.mli | |
| parent | be4f29c6d62ecef7c8736c1cd154616d3ef5292c (diff) | |
Names: revised representation of constants and mutual_inductive
- a module KernelPair for improving sharing between constant and mind
- shorter representation than a pair when possible
- exports comparisions on constant and mind and ...
- a kn_equal function instead of Int.equal (kn_ord ...) 0
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16217 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index a51ac0ad86..f704b91ba0 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -210,6 +210,7 @@ val string_of_kn : kernel_name -> string val pr_kn : kernel_name -> Pp.std_ppcmds val kn_ord : kernel_name -> kernel_name -> int +val kn_equal : kernel_name -> kernel_name -> bool module KNset : Set.S with type elt = kernel_name module KNpred : Predicate.S with type elt = kernel_name @@ -251,6 +252,8 @@ val user_con : constant -> kernel_name val canonical_con : constant -> kernel_name val repr_con : constant -> module_path * Dir_path.t * Label.t val eq_constant : constant -> constant -> bool +val con_ord : constant -> constant -> int +val con_user_ord : constant -> constant -> int val con_with_label : constant -> Label.t -> constant val string_of_con : constant -> string @@ -271,6 +274,8 @@ val user_mind : mutual_inductive -> kernel_name val canonical_mind : mutual_inductive -> kernel_name val repr_mind : mutual_inductive -> module_path * Dir_path.t * Label.t val eq_mind : mutual_inductive -> mutual_inductive -> bool +val mind_ord : mutual_inductive -> mutual_inductive -> int +val mind_user_ord : mutual_inductive -> mutual_inductive -> int val string_of_mind : mutual_inductive -> string val mind_label : mutual_inductive -> Label.t @@ -289,7 +294,11 @@ val ith_constructor_of_inductive : inductive -> int -> constructor val inductive_of_constructor : constructor -> inductive val index_of_constructor : constructor -> int val eq_ind : inductive -> inductive -> bool +val ind_ord : inductive -> inductive -> int +val ind_user_ord : inductive -> inductive -> int val eq_constructor : constructor -> constructor -> bool +val constructor_ord : constructor -> constructor -> int +val constructor_user_ord : constructor -> constructor -> int (** Better to have it here that in Closure, since required in grammar.cma *) type evaluable_global_reference = |