From 481494be9f20d9c497e4d7ac108ae19bbaa53201 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 16 Feb 2007 19:15:18 +0000
Subject: Add 'dest obj as pat in body' keyword as a pattern-matching shortcut.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9655 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_constr.ml4 | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 1a721a2e39..e05fe036d2 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -21,7 +21,7 @@ open Util
 
 let constr_kw =
   [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; 
-    "end"; "as"; "let"; "if"; "then"; "else"; "return";
+    "end"; "as"; "let"; "dest"; "if"; "then"; "else"; "return";
     "Prop"; "Set"; "Type"; ".("; "_"; ".." ]
 
 let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
@@ -195,6 +195,10 @@ GEXTEND Gram
 	  ":="; c1 = operconstr LEVEL "200"; "in";
           c2 = operconstr LEVEL "200" ->
           CLetTuple (loc,List.map snd lb,po,c1,c2)
+      | "dest"; c1 = operconstr LEVEL "200"; "as"; p=pattern;
+          "in"; c2 = operconstr LEVEL "200" ->
+         CCases (loc, None, [(c1, (None, None))],
+                 [loc, [[p]], c2])
       | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
-- 
cgit v1.2.3