diff options
| -rw-r--r-- | library/goptions.ml | 2 | ||||
| -rwxr-xr-x | library/nametab.ml | 9 | ||||
| -rwxr-xr-x | library/nametab.mli | 5 | ||||
| -rw-r--r-- | library/opaque.ml | 7 | ||||
| -rw-r--r-- | parsing/printer.ml | 7 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 8 |
6 files changed, 23 insertions, 15 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 0eae518b4..95336c35e 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -302,7 +302,7 @@ let msg_option_value (name,v) = | BoolValue false -> [< 'sTR "false" >] | IntValue n -> [< 'iNT n >] | StringValue s -> [< 'sTR s >] - | IdentValue id -> pr_sp(Nametab.sp_of_global (Global.env())id) + | IdentValue r -> pr_global_env (Global.env()) r let print_option_value key = let (name,(_,read,_)) = get_option key in diff --git a/library/nametab.ml b/library/nametab.ml index 9348ff30d..f70d672f8 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -280,7 +280,7 @@ let exists_section dir = (* For a sp Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and Coq.A.B.x is a qualid that denotes the same object. *) -let qualid_of_global env ref = +let shortest_qualid_of_global env ref = let sp = sp_of_global env ref in let (pth,id) = repr_path sp in let rec find_visible dir qdir = @@ -292,6 +292,13 @@ let qualid_of_global env ref = in find_visible (repr_dirpath pth) (make_dirpath []) +let pr_global_env env ref = + (* Il est important de laisser le let-in, car les streams s'évaluent + paresseusement : il faut forcer l'évaluation pour capturer + l'éventuelle levée d'une exception (le cas échoit dans le debugger) *) + let s = string_of_qualid (shortest_qualid_of_global env ref) in + [< 'sTR s >] + (********************************************************************) (********************************************************************) diff --git a/library/nametab.mli b/library/nametab.mli index 6cf3f8673..adb764fcb 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -46,7 +46,10 @@ val pr_qualid : qualid -> std_ppcmds val qualid_of_sp : section_path -> qualid (* Turns an absolute name into a qualified name denoting the same name *) -val qualid_of_global : Environ.env -> global_reference -> qualid +val shortest_qualid_of_global : Environ.env -> global_reference -> qualid + +(* Printing of global references using names as short as possible *) +val pr_global_env : Environ.env -> global_reference -> std_ppcmds exception GlobalizationError of qualid exception GlobalizationConstantError of qualid diff --git a/library/opaque.ml b/library/opaque.ml index c672454a5..ff551ce55 100644 --- a/library/opaque.ml +++ b/library/opaque.ml @@ -10,6 +10,7 @@ (*i*) open Util +open Pp open Names open Closure open Summary @@ -49,8 +50,10 @@ let set_transparent_const sp = let (ids,sps) = !tr_state in let cb = Global.lookup_constant sp in if cb.const_body <> None & cb.const_opaque then - let s = string_of_path sp in - error ("Cannot make "^s^" transparent because it was declared opaque."); + errorlabstrm "set_transparent_const" + [< 'sTR "Cannot make"; 'sPC; + Nametab.pr_global_env (Global.env()) (Nametab.ConstRef sp); + 'sPC; 'sTR "transparent because it was declared opaque." >]; tr_state := (ids, Sppred.add sp sps) let set_opaque_var id = diff --git a/parsing/printer.ml b/parsing/printer.ml index 3e664806d..76c0995a5 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -26,12 +26,7 @@ let emacs_str s = if !Options.print_emacs then s else "" let dfltpr ast = [< 'sTR"#GENTERM " ; print_ast ast >];; -let pr_global ref = - (* Il est important de laisser le let-in, car les streams s'évaluent - paresseusement : il faut forcer l'évaluation pour capturer - l'éventuelle levée d'une exception (le cas échoit dans le debugger) *) - let s = string_of_id (id_of_global (Global.env()) ref) in - [< 'sTR s >] +let pr_global ref = pr_global_env (Global.env()) ref let global_const_name sp = try pr_global (ConstRef sp) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 405e2e16b..714b7f682 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -31,9 +31,9 @@ let encode_inductive ref = let indsp = match ref with | IndRef indsp -> indsp | _ -> - let id = basename (Nametab.sp_of_global (Global.env()) ref) in errorlabstrm "indsp_of_id" - [< pr_id id; 'sTR" is not an inductive type" >] in + [< pr_global_env (Global.env()) ref; + 'sTR" is not an inductive type" >] in let (mib,mip) = Global.lookup_inductive indsp in let constr_lengths = Array.map List.length mip.mind_listrec in (indsp,constr_lengths) @@ -83,7 +83,7 @@ module PrintingCasesIf = let field = "If" let title = "Types leading to pretty-printing of Cases using a `if' form: " let member_message ref b = - let s = string_of_id (basename (sp_of_global (Global.env()) ref)) in + let s = string_of_qualid(shortest_qualid_of_global (Global.env()) ref) in if b then "Cases on elements of " ^ s ^ " are printed using a `if' form" else @@ -98,7 +98,7 @@ module PrintingCasesLet = let title = "Types leading to a pretty-printing of Cases using a `let' form:" let member_message ref b = - let s = string_of_id (basename (sp_of_global (Global.env()) ref)) in + let s = string_of_qualid(shortest_qualid_of_global (Global.env()) ref) in if b then "Cases on elements of " ^ s ^ " are printed using a `let' form" else |