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 /vernac | |
| 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 'vernac')
| -rw-r--r-- | vernac/assumptions.ml | 8 | ||||
| -rw-r--r-- | vernac/classes.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 3 |
3 files changed, 6 insertions, 7 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index b000745961..15c0278f47 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -119,7 +119,7 @@ and fields_of_expression x = fields_of_functor fields_of_expr x let lookup_constant_in_impl cst fallback = try - let mp,dp,lab = KerName.repr (Constant.canonical cst) in + let mp,lab = KerName.repr (Constant.canonical cst) in let fields = memoize_fields_of_mp mp in (* A module found this way is necessarily closed, in particular our constant cannot be in an opened section : *) @@ -143,7 +143,7 @@ let lookup_constant cst = let lookup_mind_in_impl mind = try - let mp,dp,lab = KerName.repr (MutInd.canonical mind) in + let mp,lab = KerName.repr (MutInd.canonical mind) in let fields = memoize_fields_of_mp mp in search_mind_label lab fields with Not_found -> @@ -157,9 +157,9 @@ let lookup_mind mind = traversed objects *) let label_of = function - | ConstRef kn -> pi3 (Constant.repr3 kn) + | ConstRef kn -> Constant.label kn | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> pi3 (MutInd.repr3 kn) + | ConstructRef ((kn,_),_) -> MutInd.label kn | VarRef id -> Label.of_id id let fold_constr_with_full_binders g f n acc c = diff --git a/vernac/classes.ml b/vernac/classes.ml index c738d14af9..37ee33b19f 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -99,7 +99,7 @@ let type_ctx_instance env sigma ctx inst subst = let id_of_class cl = match cl.cl_impl with - | ConstRef kn -> let _,_,l = Constant.repr3 kn in Label.to_id l + | ConstRef kn -> Label.to_id @@ Constant.label kn | IndRef (kn,i) -> let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in mip.(0).Declarations.mind_typename diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 015d5fabef..cf2fecb9c1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -249,8 +249,7 @@ let print_namespace ns = in let print_list pr l = prlist_with_sep (fun () -> str".") pr l in let print_kn kn = - (* spiwack: I'm ignoring the dirpath, is that bad? *) - let (mp,_,lbl) = Names.KerName.repr kn in + let (mp,lbl) = Names.KerName.repr kn in let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in print_list Id.print qn in |