diff options
| author | Maxime Dénès | 2018-09-25 14:33:46 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-05 08:57:56 +0200 |
| commit | 650c65af484c45f4e480252b55d148bcc198be6c (patch) | |
| tree | ebc0a8e7777ddd90515abcdea2e8975d1d968640 /kernel/names.mli | |
| parent | 3f2a6d8e99f31bbd9383119cac39ed0bcaabc37d (diff) | |
[kernel] Remove section paths from `KerName.t`
We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.
Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 16 |
1 files changed, 6 insertions, 10 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 2ea8108734..2145a51c4e 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -274,9 +274,11 @@ sig type t (** Constructor and destructor *) - val make : ModPath.t -> DirPath.t -> Label.t -> t + val make : ModPath.t -> Label.t -> t + val repr : t -> ModPath.t * Label.t + val make2 : ModPath.t -> Label.t -> t - val repr : t -> ModPath.t * DirPath.t * Label.t + [@@ocaml.deprecated "Please use [KerName.make]"] (** Projections *) val modpath : t -> ModPath.t @@ -317,15 +319,12 @@ sig val make2 : ModPath.t -> Label.t -> t (** Shortcut for [(make1 (KerName.make2 ...))] *) - val make3 : ModPath.t -> DirPath.t -> Label.t -> t - (** Shortcut for [(make1 (KerName.make ...))] *) - (** Projections *) val user : t -> KerName.t val canonical : t -> KerName.t - val repr3 : t -> ModPath.t * DirPath.t * Label.t + val repr2 : t -> ModPath.t * Label.t (** Shortcut for [KerName.repr (user ...)] *) val modpath : t -> ModPath.t @@ -403,15 +402,12 @@ sig val make2 : ModPath.t -> Label.t -> t (** Shortcut for [(make1 (KerName.make2 ...))] *) - val make3 : ModPath.t -> DirPath.t -> Label.t -> t - (** Shortcut for [(make1 (KerName.make ...))] *) - (** Projections *) val user : t -> KerName.t val canonical : t -> KerName.t - val repr3 : t -> ModPath.t * DirPath.t * Label.t + val repr2 : t -> ModPath.t * Label.t (** Shortcut for [KerName.repr (user ...)] *) val modpath : t -> ModPath.t |