diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-30 12:02:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-30 12:02:32 +0000 |
| commit | 306d1be283442c361aa26d000d339f3f4dfbeab9 (patch) | |
| tree | 5fdec06c70ef551f8b775988820fb07c7538e29f /parsing/ppconstr.mli | |
| parent | 77d86619f5f557de52a391f6811bacd73c01580b (diff) | |
Fixing bug #2146 (broken selection of occurrences in "change").
In trunk the different possible combinations of "at" and "in" with
occurrences are taken into account.
In 8.2 branch, it remains fragile (syntaxes that were accepted remain
accepted and a message warns if the occurrences coming after the
"with" are not taken into account).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12614 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppconstr.mli')
| -rw-r--r-- | parsing/ppconstr.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index f107d5984..1aa173e24 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -54,8 +54,6 @@ val pr_qualid : qualid -> std_ppcmds val pr_with_occurrences : ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds -val pr_with_occurrences_with_trailer : - ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds -> std_ppcmds val pr_red_expr : ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) -> ('a,'b,'c) red_expr_gen -> std_ppcmds |