diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-17 20:28:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-17 20:28:23 +0000 |
| commit | 6b391cc61a35d1ef42f88d18f9c428c369180493 (patch) | |
| tree | c402fcb05a8dd450dca2191607c11351633cfac0 /interp/notation.mli | |
| parent | 9d7a9ab7c8182dff99d5afd078747f5d6b1247f0 (diff) | |
Fixed a notation bug when extending binder_constr with empty levels
(see Notations.v).
Improved the "already occurs in a different scope" test and message.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12399 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.mli b/interp/notation.mli index f3036f226..3dc3c95c2 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -164,7 +164,7 @@ type symbol = val make_notation_key : symbol list -> notation val decompose_notation_key : notation -> symbol list -(* Prints scopes (expect a pure aconstr printer *) +(* Prints scopes (expects a pure aconstr printer) *) val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds val locate_notation : (rawconstr -> std_ppcmds) -> notation -> |