diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-10 07:19:28 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-10 07:19:28 +0000 |
| commit | 79dc33cbc403ebab0bd1fe815c13f740f0a1b850 (patch) | |
| tree | e38e167003d7dd97d95a59ea7c026a1629b346f8 /syntax | |
| parent | c0ff579606f2eba24bc834316d8bb7bcc076000d (diff) | |
Ajout d'un LetIn primitif.
Abstraction de constr via kind_of_constr dans une bonne partie du code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'syntax')
| -rwxr-xr-x | syntax/PPConstr.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v index ad74cd462..25f8a2c7f 100755 --- a/syntax/PPConstr.v +++ b/syntax/PPConstr.v @@ -129,6 +129,7 @@ Syntax constr | lambdal_cons [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body)] -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) $id) $body)] + | letin [<<[$x = $A] $B>>] -> [ [ <hov 0> "[" $x ":=" $A "]" [0 1] $B:E ] ] | pi [<<($x : $A)$B>>] -> [(PRODBOX (BINDERS) <<($x : $A)$B>>)] | prodlist [(PRODLIST $c $b)] |