diff options
| -rw-r--r-- | kernel/environ.ml | 14 | ||||
| -rw-r--r-- | kernel/environ.mli | 9 |
2 files changed, 15 insertions, 8 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index d95a87253..ed74f0f2d 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -202,20 +202,24 @@ let lookup_mind sp env = let lowercase_first_char id = String.lowercase (first_char id) (* id_of_global gives the name of the given sort oper *) -let id_of_global env = function - | ConstRef sp -> - basename sp +let sp_of_global env = function + | VarRef sp -> sp + | ConstRef sp -> sp | IndRef (sp,tyi) -> (* Does not work with extracted inductive types when the first inductive is logic : if tyi=0 then basename sp else *) let mib = lookup_mind sp env in let mip = mind_nth_type_packet mib tyi in - mip.mind_typename + make_path (dirpath sp) mip.mind_typename CCI | ConstructRef ((sp,tyi),i) -> let mib = lookup_mind sp env in let mip = mind_nth_type_packet mib tyi in assert (i <= Array.length mip.mind_consnames && i > 0); - mip.mind_consnames.(i-1) + make_path (dirpath sp) mip.mind_consnames.(i-1) CCI + | EvarRef n -> + make_path [] (id_of_string ("?"^(string_of_int n))) CCI + +let id_of_global env ref = basename (sp_of_global env ref) let hdchar env c = let rec hdrec k c = diff --git a/kernel/environ.mli b/kernel/environ.mli index 84f384759..7e90dd4cd 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -94,13 +94,16 @@ val lookup_rel_value : int -> env -> constr option (* Looks up in the context of global constant names *) (* raises [Not_found] if the required path is not found *) -val lookup_constant : section_path -> env -> constant_body +val lookup_constant : constant_path -> env -> constant_body (* Looks up in the context of global inductive names *) (* raises [Not_found] if the required path is not found *) val lookup_mind : section_path -> env -> mutual_inductive_body (*s Miscellanous *) + +val sp_of_global : env -> global_reference -> section_path + val id_of_global : env -> global_reference -> identifier val make_all_name_different : env -> env @@ -146,8 +149,8 @@ val evaluable_constant : env -> constant -> bool (*s Opaque / Transparent switching *) -val set_opaque : env -> section_path -> unit -val set_transparent : env -> section_path -> unit +val set_opaque : env -> constant_path -> unit +val set_transparent : env -> constant_path -> unit (*s Modules. *) |