diff options
| author | herbelin | 2002-11-03 14:04:55 +0000 |
|---|---|---|
| committer | herbelin | 2002-11-03 14:04:55 +0000 |
| commit | 079f42ac05f7900001e2e77ce615103e089fa2b6 (patch) | |
| tree | 8b82052ec52d858777c80135f19e39ac17913623 | |
| parent | e206cbc6b24da23fc8edd06fae70a75bd868c59a (diff) | |
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
| -rw-r--r-- | parsing/coqast.ml | 2 | ||||
| -rw-r--r-- | parsing/coqast.mli | 1 |
2 files changed, 3 insertions, 0 deletions
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 |