1 files changed, 77 insertions, 0 deletions
diff --git a/interp/symbols.mli b/interp/symbols.mli
new file mode 100644
index 000000000..3c082b2ce
--- /dev/null
+++ b/interp/symbols.mli
@@ -0,0 +1,77 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(*i*)
+open Util
+open Pp
+open Bignat
+open Names
+open Nametab
+open Rawterm
+open Topconstr
+open Ppextend
+(*i*)
+
+(*s A numeral interpreter is the pair of an interpreter for _integer_
+   numbers in terms and an optional interpreter in pattern, if
+   negative numbers are not supported, the interpreter must fail with
+   an appropriate error message *)
+
+type numeral_interpreter_name = string
+type numeral_interpreter =
+    (loc -> bigint -> rawconstr)
+    * (loc -> bigint -> name -> cases_pattern) option
+
+(* A scope is a set of interpreters for symbols + optional
+   interpreter and printers for integers + optional delimiters *)
+
+type level = precedence * precedence list
+type delimiters = string * string
+type scope
+type scopes = scope_name list
+
+val default_scope : scope_name
+val current_scopes : unit -> scopes
+val open_scope : scope_name -> unit
+val declare_scope : scope_name -> unit
+
+(* Declare delimiters for printing *)
+val declare_delimiters : scope_name -> delimiters -> unit
+
+(* Declare, interpret, and look for a printer for numeral *)
+val declare_numeral_interpreter :
+  numeral_interpreter_name -> numeral_interpreter -> unit
+val interp_numeral : loc -> bigint -> scopes -> rawconstr
+val interp_numeral_as_pattern : loc -> bigint -> name -> scopes ->cases_pattern
+val find_numeral_printer : string -> scopes ->
+  (delimiters option * scopes) option
+
+(* Declare, interpret, and look for a printer for symbolic notations *)
+val declare_notation : notation -> scope_name -> aconstr * level -> unit
+val interp_notation : notation -> scopes -> aconstr
+val find_notation : scope_name -> notation -> scopes -> 
+  (delimiters option * scopes) option
+val exists_notation_in_scope : 
+  scope_name -> level -> notation -> aconstr -> bool
+val exists_notation : level -> notation -> bool
+
+(* Declare and look for scopes associated to arguments of a global ref *)
+open Libnames
+val declare_arguments_scope: global_reference -> scope_name option list -> unit
+val find_arguments_scope : global_reference -> scope_name option list
+
+(* Printing scopes *)
+val pr_scope : (aconstr -> std_ppcmds) -> scope_name -> std_ppcmds
+val pr_scopes : (aconstr -> std_ppcmds) -> std_ppcmds
+
+
+val declare_printing_rule : notation -> unparsing list * precedence -> unit
+val find_notation_printing_rule : notation -> unparsing list * precedence
+