From baa3e16836c3f0daf24ba47aadbdee525762d6ec Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 9 Dec 1999 23:20:18 +0000
Subject: 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
---
 syntax/PPCommand.v | 28 +++++++++++++++++++++++++++-
 1 file changed, 27 insertions(+), 1 deletion(-)

(limited to 'syntax')

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>>)]
-- 
cgit v1.2.3