diff options
Diffstat (limited to 'interp/dumpglob.ml')
| -rw-r--r-- | interp/dumpglob.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index c7d3da653c..931fc1ca40 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -141,7 +141,7 @@ let interval loc = let dump_ref loc filepath modpath ident ty = match !glob_output with | Feedback -> - Pp.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty)) + Feedback.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty)) | NoGlob -> () | _ when not (Loc.is_ghost loc) -> let bl,el = interval loc in @@ -172,7 +172,7 @@ let cook_notation df sc = (* - all single quotes in terminal tokens are doubled *) (* - characters < 32 are represented by '^A, '^B, '^C, etc *) (* The output is decoded in function Index.prepare_entry of coqdoc *) - let ntn = String.make (String.length df * 3) '_' in + let ntn = String.make (String.length df * 5) '_' in let j = ref 0 in let l = String.length df - 1 in let i = ref 0 in @@ -240,7 +240,7 @@ let dump_binding loc id = () let dump_def ty loc secpath id = if !glob_output = Feedback then - Pp.feedback (Feedback.GlobDef (loc, id, secpath, ty)) + Feedback.feedback (Feedback.GlobDef (loc, id, secpath, ty)) else let bl,el = interval loc in dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el secpath id) @@ -248,7 +248,7 @@ let dump_def ty loc secpath id = let dump_definition (loc, id) sec s = dump_def s loc (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id) -let dump_constraint ((loc, n), _, _) sec ty = +let dump_constraint (((loc, n),_), _, _) sec ty = match n with | Names.Name id -> dump_definition (loc, id) sec ty | Names.Anonymous -> () |