diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-06-29 10:05:56 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-29 10:05:56 +0200 |
commit | fc4f18c84bfc421dff55c77aa564abc1ea20f528 (patch) | |
tree | 4a9656e44d957f17a8c342e794a8bf2276ea50f3 /vernac | |
parent | 092b74035b73780432a1db9588a7ac54ec6a4721 (diff) | |
parent | e7e3714f0fd0e791501acccca3317ed8175c4815 (diff) |
Merge PR #7745: Make type Environ.globals abstract + simplify Environ.retroknowledge
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/vernacentries.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 43c974846..6d1abeca1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -263,15 +263,13 @@ let print_namespace ns = let matches mp = match match_modulepath ns mp with | Some [] -> true | _ -> false in - let constants = (Global.env ()).Environ.env_globals.Environ.env_constants in let constants_in_namespace = - Cmap_env.fold (fun c (body,_) acc -> - let kn = Constant.user c in - if matches (KerName.modpath kn) then - acc++fnl()++hov 2 (print_constant kn body) - else - acc - ) constants (str"") + Environ.fold_constants (fun c body acc -> + let kn = Constant.user c in + if matches (KerName.modpath kn) + then acc++fnl()++hov 2 (print_constant kn body) + else acc) + (Global.env ()) (str"") in (print_list Id.print ns)++str":"++fnl()++constants_in_namespace |