diff options
Diffstat (limited to 'interp/dumpglob.ml')
| -rw-r--r-- | interp/dumpglob.ml | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index d7962e29a6..bc6a1ef3aa 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util @@ -249,12 +251,12 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc -> dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el secpath id) ) loc -let dump_definition (loc, id) sec s = +let dump_definition {CAst.loc;v=id} sec s = dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id) -let dump_constraint (((loc, n),_), _, _) sec ty = +let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty = match n with - | Names.Name id -> dump_definition (loc, id) sec ty + | Names.Name id -> dump_definition CAst.(make ?loc id) sec ty | Names.Anonymous -> () let dump_moddef ?loc mp ty = |