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 /pretyping/classops.ml | |
| 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 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index b264e31474..b026397abf 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -451,12 +451,6 @@ let subst_coercion (subst, c) = else { c with coercion_type = coe; coercion_source = cls; coercion_target = clt; coercion_is_proj = clp; } -let discharge_cl = function - | CL_CONST kn -> CL_CONST (Lib.discharge_con kn) - | CL_IND ind -> CL_IND (Lib.discharge_inductive ind) - | CL_PROJ p -> CL_PROJ (Lib.discharge_proj_repr p) - | cl -> cl - let discharge_coercion (_, c) = if c.coercion_local then None else @@ -467,9 +461,6 @@ let discharge_coercion (_, c) = with Not_found -> 0 in let nc = { c with - coercion_type = Lib.discharge_global c.coercion_type; - coercion_source = discharge_cl c.coercion_source; - coercion_target = discharge_cl c.coercion_target; coercion_params = n + c.coercion_params; coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj; } in |