diff options
| author |  Matej Kosik <matej.kosik@inria.fr> | 2016-10-25 13:40:18 +0200 |
|---|---|---|
| committer | Matej Kosik <matej.kosik@inria.fr> | 2016-10-26 10:55:32 +0200 |
| commit | 68dfa4701d7636728270dfd8f33133627486204b (patch) | |
| tree | 9b8f95fd7e6cdc2aa6afdcea3fcc3cf38730503b /kernel | |
| parent | 5474d83bc8845bd5aa3fb339057d6efa5feedd7a (diff) | |
COMMENT: Names.Cmap and Names.Cmap_env
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 6 | ||||
| -rw-r--r-- | kernel/names.mli | 6 |
2 files changed, 12 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 1313bae7b..d928d300f 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -598,7 +598,13 @@ end module Constant = KerPair module Cmap = HMap.Make(Constant.CanOrd) +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "cannonical form" of the constant. *) + module Cmap_env = HMap.Make(Constant.UserOrd) +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "user form" of the constant. *) + module Cpred = Predicate.Make(Constant.CanOrd) module Cset = Cmap.Set module Cset_env = Cmap_env.Set diff --git a/kernel/names.mli b/kernel/names.mli index 0af1cde8f..6b0a80625 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -371,8 +371,14 @@ end module Cpred : Predicate.S with type elt = Constant.t module Cset : CSig.SetS with type elt = Constant.t module Cset_env : CSig.SetS with type elt = Constant.t + module Cmap : Map.ExtS with type key = Constant.t and module Set := Cset +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "cannonical form" of the constant. *) + module Cmap_env : Map.ExtS with type key = Constant.t and module Set := Cset_env +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "user form" of the constant. *) (** {6 Inductive names} *) |