diff options
| author | herbelin | 1999-12-09 23:20:18 +0000 |
|---|---|---|
| committer | herbelin | 1999-12-09 23:20:18 +0000 |
| commit | baa3e16836c3f0daf24ba47aadbdee525762d6ec (patch) | |
| tree | 4841eb29be562802e06f9aa3f72ccda37daa5814 /syntax | |
| parent | 35c127288df53b8561d13082738806fa44049a1a (diff) | |
Ajout des messages d'erreurs de Cases
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@226 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'syntax')
| -rwxr-xr-x | syntax/PPCommand.v | 28 |
1 files changed, 27 insertions, 1 deletions
diff --git a/syntax/PPCommand.v b/syntax/PPCommand.v index 0033807bd1..7df18f7be4 100755 --- a/syntax/PPCommand.v +++ b/syntax/PPCommand.v @@ -71,7 +71,7 @@ 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)] @@ -93,6 +93,32 @@ Syntax constr -> [(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)] + | lambda_anon [(LAMBDA $Dom [<>]$Body)] + -> [(LAMBOX (BINDERS (BINDER $Dom _)) $Body)] + | lambdalist [(LAMBDALIST $c [$x]$body)] + -> [(LAMLBOX (BINDERS) $c (IDS $x) $body)] + | lambdalist_anon [(LAMBDALIST $c [<>]$body)] + -> [(LAMLBOX (BINDERS) $c (IDS _) $body)] + + | formated_lambda [(LAMBOX $pbi $t)] + -> [ [<hov 0> "[" [<hv 0> $pbi] "]" [0 1] $t:E ] ] + + | lambda_cons [(LAMBOX (BINDERS ($LIST $acc)) (LAMBDA $Dom [$x]$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)] | pi [<<($x : $A)$B>>] -> [(PRODBOX (BINDERS) <<($x : $A)$B>>)] |