diff options
| author | herbelin | 2009-09-11 17:53:30 +0000 |
|---|---|---|
| committer | herbelin | 2009-09-11 17:53:30 +0000 |
| commit | ea85f46dc0cc34db149c24bb2da8f3130e191fc1 (patch) | |
| tree | 3b8fa67f3f1dc5bb2815b38c1040a3ea192c88fe /parsing/prettyp.mli | |
| parent | 7131609a82198080421b15e2c7a0d8f3b6cbd3de (diff) | |
Generalized the possibility to refer to a global name by a notation
string in most commands expecting a global name (e.g. 'Print "+"' for
an infix notation or 'Print "{ _ } + { _ }"' for a misfix notation,
possibly surrounded by a scope delimiter). Support for such smart
globals in VERNAC EXTEND to do.
Added a file smartlocate.ml for high-level globalization functions.
Mini-nettoyage metasyntax.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12323 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/prettyp.mli')
| -rw-r--r-- | parsing/prettyp.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 88b0a80ecc..ba1977e893 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -18,6 +18,7 @@ open Environ open Reductionops open Libnames open Nametab +open Genarg (*i*) (* A Pretty-Printer for the Calculus of Inductive Constructions. *) @@ -40,10 +41,10 @@ val print_eval : (* This function is exported for the graphical user-interface pcoq *) val build_inductive : mutual_inductive -> int -> global_reference * rel_context * types * identifier array * types array -val print_name : reference -> std_ppcmds +val print_name : reference or_by_notation -> std_ppcmds val print_opaque_name : reference -> std_ppcmds -val print_about : reference -> std_ppcmds -val print_impargs : reference -> std_ppcmds +val print_about : reference or_by_notation -> std_ppcmds +val print_impargs : reference or_by_notation -> std_ppcmds (*i val print_extracted_name : identifier -> std_ppcmds |