diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-06 14:22:34 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-06 14:22:34 +0100 |
| commit | 1afa595012bbaf5fb89398b355f16159e1af399b (patch) | |
| tree | 255cc594c736debd1cbd53b92906e1fa10d80de5 /kernel/names.mli | |
| parent | 7ca0319268c2c6912e08c53deb742d5f7631e210 (diff) | |
| parent | 8b5d02d8706f99015c2ce8efcad32b7af228dd53 (diff) | |
Merge remote-tracking branch 'origin/v8.5' into trunk
Conflicts:
lib/cSig.mli
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index b128fe335..38a51a392 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -409,7 +409,7 @@ end module Mindset : CSig.SetS with type elt = MutInd.t module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset -module Mindmap_env : Map.S with type key = MutInd.t +module Mindmap_env : CSig.MapS with type key = MutInd.t (** Beware: first inductive has index 0 *) type inductive = MutInd.t * int @@ -417,10 +417,10 @@ type inductive = MutInd.t * int (** Beware: first constructor has index 1 *) type constructor = inductive * int -module Indmap : Map.S with type key = inductive -module Constrmap : Map.S with type key = constructor -module Indmap_env : Map.S with type key = inductive -module Constrmap_env : Map.S with type key = constructor +module Indmap : CSig.MapS with type key = inductive +module Constrmap : CSig.MapS with type key = constructor +module Indmap_env : CSig.MapS with type key = inductive +module Constrmap_env : CSig.MapS with type key = constructor val ind_modpath : inductive -> ModPath.t val constr_modpath : constructor -> ModPath.t |