From 68dfa4701d7636728270dfd8f33133627486204b Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 25 Oct 2016 13:40:18 +0200 Subject: COMMENT: Names.Cmap and Names.Cmap_env --- kernel/names.mli | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'kernel/names.mli') 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} *) -- cgit v1.2.3