diff options
| author | gmelquio | 2009-11-04 18:47:36 +0000 |
|---|---|---|
| committer | gmelquio | 2009-11-04 18:47:36 +0000 |
| commit | 208eceab14148fa561c36f71e2e1485e73832616 (patch) | |
| tree | 3763b73a349cca213cee543f8cf0204d65594ae6 /interp/topconstr.ml | |
| parent | fc7f18e8596a8b4e690ff726edb02a7cf319edbd (diff) | |
Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.
Fixed pretty printing of record syntax.
Allowed record syntax inside patterns. (Patch by Cedric Auger.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12468 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/topconstr.ml')
| -rw-r--r-- | interp/topconstr.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index ec1b20a12b..04715d51b3 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -634,6 +634,7 @@ type cases_pattern_expr = | CPatOr of loc * cases_pattern_expr list | CPatNotation of loc * notation * cases_pattern_expr notation_substitution | CPatPrim of loc * prim_token + | CPatRecord of loc * (reference * cases_pattern_expr) list | CPatDelimiters of loc * string * cases_pattern_expr type constr_expr = @@ -647,7 +648,7 @@ type constr_expr = | CAppExpl of loc * (proj_flag * reference) * constr_expr list | CApp of loc * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list - | CRecord of loc * constr_expr option * (identifier located * constr_expr) list + | CRecord of loc * constr_expr option * (reference * constr_expr) list | CCases of loc * case_style * constr_expr option * (constr_expr * (name option * constr_expr option)) list * (loc * cases_pattern_expr list located list * constr_expr) list @@ -743,6 +744,7 @@ let cases_pattern_expr_loc = function | CPatAtom (loc,_) -> loc | CPatOr (loc,_) -> loc | CPatNotation (loc,_,_) -> loc + | CPatRecord (loc, _) -> loc | CPatPrim (loc,_) -> loc | CPatDelimiters (loc,_,_) -> loc @@ -774,6 +776,8 @@ let is_constructor id = with Not_found -> true let rec cases_pattern_fold_names f a = function + | CPatRecord (_, l) -> + List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l | CPatAlias (_,pat,id) -> f id a | CPatCstr (_,_,patl) | CPatOr (_,patl) -> List.fold_left (cases_pattern_fold_names f) a patl |