diff options
| author | herbelin | 2000-10-05 19:30:25 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-05 19:30:25 +0000 |
| commit | 924a98d1a98cdaddf459be9ea4ea82b651dec55e (patch) | |
| tree | e9df195725b16510a34cff1eadb16dfb767520dc | |
| parent | 43c3459cedee2476ca0739d1e88f8738b4d64ea7 (diff) | |
Code mort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@662 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rwxr-xr-x | syntax/PPConstr.v | 25 |
1 files changed, 1 insertions, 24 deletions
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v index f8c8447afb..9b37f4aa70 100755 --- a/syntax/PPConstr.v +++ b/syntax/PPConstr.v @@ -83,31 +83,8 @@ Syntax constr (* Things parsed in command7 *) (* Things parsed in command8 *) level 8: -(* - lambda [(LAMBDA $Dom $Body)] - -> [(LAMBOX (BINDERS) (LAMBDA $Dom $Body))] - | lambdalist [(LAMBDALIST $c $body)] - -> [(LAMBOX (BINDERS) (LAMBDALIST $c $body))] - - | formated_lambda [(LAMBOX $pbi $t)] - -> [ [<hov 0> "[" [<hv 0> $pbi] "]" [0 1] $t:E ] ] - - | lambda_cons [(LAMBOX (BINDERS ($LIST $acc)) <<[$x : $Dom]$body>>)] - -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $Dom $x)) $body)] - | lambda_cons_anon [(LAMBOX (BINDERS ($LIST $acc)) (LAMBDA $Dom [<>]$body))] - -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $Dom _)) $body)] - | lambdal_start [(LAMBOX $pbi (LAMBDALIST $Dom $Body))] - -> [(LAMLBOX $pbi $Dom (IDS) $Body)] - - | lambdal_end [(LAMLBOX (BINDERS ($LIST $acc)) $c (IDS ($LIST $ids)) $t)] - -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $c ($LIST $ids))) $t)] - | lambdal_cons_anon [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [<>]$body)] - -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) _) $body)] - | lambdal_cons [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body)] - -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) $id) $body)] -*) lambda [(LAMBDA $Dom [$x]$Body)] - -> [(LAMBOX (BINDERS (BINDER $Dom $x)) $Body)] + -> [(LAMBOX (BINDERS (BINDER $Dom $x)) $body)] | lambda_anon [(LAMBDA $Dom [<>]$Body)] -> [(LAMBOX (BINDERS (BINDER $Dom _)) $Body)] | lambdalist [(LAMBDALIST $c [$x]$body)] |
