diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /interp/dumpglob.mli | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'interp/dumpglob.mli')
| -rw-r--r-- | interp/dumpglob.mli | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index a0666c81..f6d7baef 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: dumpglob.mli 11582 2008-11-12 19:49:57Z notin $ *) +(* $Id$ *) val open_glob_file : string -> unit @@ -23,8 +23,9 @@ val dump_to_dotglob : unit -> unit val pause : unit -> unit val continue : unit -> unit -val coqdoc_freeze : unit -> Lexer.location_table * int * int -val coqdoc_unfreeze : Lexer.location_table * int * int -> unit +type coqdoc_state = Lexer.location_table +val coqdoc_freeze : unit -> coqdoc_state +val coqdoc_unfreeze : coqdoc_state -> unit val add_glob : Util.loc -> Libnames.global_reference -> unit val add_glob_kn : Util.loc -> Names.kernel_name -> unit @@ -34,8 +35,9 @@ val dump_moddef : Util.loc -> Names.module_path -> string -> unit val dump_modref : Util.loc -> Names.module_path -> string -> unit val dump_reference : Util.loc -> string -> string -> string -> unit val dump_libref : Util.loc -> Names.dir_path -> string -> unit -val dump_notation_location : int -> (Notation.notation_location * Topconstr.scope_name option) -> unit +val dump_notation_location : (int * int) list -> Topconstr.notation -> (Notation.notation_location * Topconstr.scope_name option) -> unit val dump_binding : Util.loc -> Names.Idset.elt -> unit +val dump_notation : Util.loc * (Topconstr.notation * Notation.notation_location) -> Topconstr.scope_name option -> bool -> unit val dump_constraint : Topconstr.typeclass_constraint -> bool -> string -> unit val dump_local_binder : Topconstr.local_binder -> bool -> string -> unit |