diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-14 08:47:23 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-14 08:47:23 +0000 |
| commit | f14c78df2be140c1c4c731d4d6010f114001b7cc (patch) | |
| tree | d79612d2f6ae903c099bc449cc04031bcff99e93 /syntax | |
| parent | 4d1cc783610c6d64e135f97e3dc860df424d8f2a (diff) | |
Parenthèses forcées autour des arguments d'une application pour parser
les expressions comme "(f (x+1))" (anticipation sur nouvelle syntaxe)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3135 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'syntax')
| -rwxr-xr-x | syntax/PPConstr.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v index 6e17c0d51..4b91f8c7b 100755 --- a/syntax/PPConstr.v +++ b/syntax/PPConstr.v @@ -174,7 +174,10 @@ Syntax constr | app_imp_last [ << (APPLISTIMPL (ACC ($LIST $A)) $T) >> ] -> [ (APPLIST ($LIST $A) $T):E ] *) + ; + (* To force parenthesis on arguments *) + level 0: | apptailcons [ << (APPTAIL $H ($LIST $T)) >> ] -> [ [1 1] $H:L (APPTAIL ($LIST $T)):E ] | apptailnil [ << (APPTAIL) >> ] -> [ ] |