diff options
| author | herbelin | 2003-04-27 18:32:34 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-27 18:32:34 +0000 |
| commit | 7ce9a2c43420d694a901c152d95b6645c76d34cd (patch) | |
| tree | 16dd4bd276ffa21f7ee30bf10a944f8b4974de0b /syntax | |
| parent | 8412d45181edd1d0627df454fa370d858d3fd623 (diff) | |
Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix permet)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3959 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'syntax')
| -rwxr-xr-x | syntax/PPConstr.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v index 0b111a69f1..492c5cbbaa 100755 --- a/syntax/PPConstr.v +++ b/syntax/PPConstr.v @@ -33,7 +33,9 @@ Syntax constr | bindersone [ << (BINDERS (BINDER $c ($LIST $id))) >> ] -> [ [<hov 0> (IDBINDER ($LIST $id))] ":" $c:E ] - | letbinder [ << (BINDERS (LETBINDER $c $id)) >> ] -> + | letbindercons [ << (BINDERS (LETBINDER $c $id) ($LIST $b)) >> ] -> + [ [<hov 0> id ":=" [0 1] $c:E ";" [1 0] (BINDERS ($LIST $b)) ] ] + | letbinderone [ << (BINDERS (LETBINDER $c $id)) >> ] -> [ [<hov 0> id ":=" [0 1] $c:E ] ] ; |