diff options
| author | herbelin | 2000-01-07 22:16:40 +0000 |
|---|---|---|
| committer | herbelin | 2000-01-07 22:16:40 +0000 |
| commit | 46e708f92deef78043f4f221293df131e29aeff1 (patch) | |
| tree | 537ac4a5b31f2d6ba510022b67b387f8cc5ddf84 /syntax | |
| parent | fb15b95d4d430ca2394a2df8da32cab8891f7e66 (diff) | |
Renommage command en constr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@262 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'syntax')
| -rwxr-xr-x | syntax/PPConstr.v (renamed from syntax/PPCommand.v) | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/syntax/PPCommand.v b/syntax/PPConstr.v index 7df18f7be4..493f3c23af 100755 --- a/syntax/PPCommand.v +++ b/syntax/PPConstr.v @@ -154,6 +154,10 @@ Syntax constr -> [ [<hov 0> $H:E (APPTAIL ($LIST $T)):E ] ] | app_imp [(APPLISTEXPL $H ($LIST $T))] + -> [ [<hov 0> "!" $H:E (APPTAIL ($LIST $T)):E ] ] + +(* + | app_imp [(APPLISTEXPL $H ($LIST $T))] -> [ (APPLISTIMPL (ACC $H) ($LIST $T)):E ] | app_imp_arg [(APPLISTIMPL (ACC ($LIST $AC)) $a ($LIST $T))] @@ -164,20 +168,21 @@ Syntax constr | app_imp_last [(APPLISTIMPL (ACC ($LIST $A)) $T)] -> [ (APPLIST ($LIST $A) $T):E ] - +*) | apptailcons [ (APPTAIL $H ($LIST $T))] -> [ [1 1] $H:L (APPTAIL ($LIST $T)):E ] | apptailnil [(APPTAIL)] -> [ ] | apptailcons1 [(APPTAIL (EXPL "!" $n $c1) ($LIST $T))] -> [ [1 1] (EXPL $n $c1):L (APPTAIL ($LIST $T)):E ] + ; (* Implicits *) level 8: arg_implicit [(EXPL ($NUM $n) $c1)] -> [ $n "!" $c1:L ] - | arg_implicit1 [(EXPL "EX" ($NUM $n) $c1)] -> [ $n "!" $c1:L ] - | fun_explicit [(EXPL $f)] -> [ $f ] +(* | arg_implicit1 [(EXPL "EX" ($NUM $n) $c1)] -> [ $n "!" $c1:L ] + | fun_explicit [(EXPL $f)] -> [ $f ]*) ; |