From 079f42ac05f7900001e2e77ce615103e089fa2b6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 3 Nov 2002 14:04:55 +0000
Subject: Ajout delimiteurs dans les motifs de Cases

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3203 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/coqast.ml  | 2 ++
 parsing/coqast.mli | 1 +
 2 files changed, 3 insertions(+)

diff --git a/parsing/coqast.ml b/parsing/coqast.ml
index cce1dba1ec..c0ecc618b0 100644
--- a/parsing/coqast.ml
+++ b/parsing/coqast.ml
@@ -140,6 +140,7 @@ type cases_pattern =
   | CPatCstr of loc * reference_expr * cases_pattern list
   | CPatAtom of loc * reference_expr option
   | CPatNumeral of loc * Bignat.bigint
+  | CPatDelimiters of loc * scope_name * cases_pattern
 
 type ordered_case_style = CIf | CLet | CMatch | CCase
 
@@ -198,6 +199,7 @@ let cases_pattern_loc = function
   | CPatCstr (loc,_,_) -> loc
   | CPatAtom (loc,_) -> loc
   | CPatNumeral (loc,_) -> loc
+  | CPatDelimiters (loc,_,_) -> loc
 
 let replace_vars_constr_ast l t =
   if l = [] then t else failwith "replace_constr_ast: TODO"
diff --git a/parsing/coqast.mli b/parsing/coqast.mli
index 817ccb5cd3..52b19c6bc7 100644
--- a/parsing/coqast.mli
+++ b/parsing/coqast.mli
@@ -69,6 +69,7 @@ type cases_pattern =
   | CPatCstr of loc * reference_expr * cases_pattern list
   | CPatAtom of loc * reference_expr option
   | CPatNumeral of loc * Bignat.bigint
+  | CPatDelimiters of loc * scope_name * cases_pattern
 
 type ordered_case_style = CIf | CLet | CMatch | CCase
 
-- 
cgit v1.2.3