diff options
| author | Pierre-Marie Pédrot | 2018-10-06 13:55:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-06 13:55:48 +0200 |
| commit | 371566f7619aed79aad55ffed6ee0920b961be6e (patch) | |
| tree | f5a7f56d5d5e924987ef0970aa0b72ec53aad673 /vernac | |
| parent | 28df7dd06dbea299736f3897ecabd2a6e3fd8e28 (diff) | |
| parent | 650c65af484c45f4e480252b55d148bcc198be6c (diff) | |
Merge PR #8555: Remove section paths from kernel names
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 |