diff options
| -rwxr-xr-x | syntax/PPConstr.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v index 47d92d95d..1c8026794 100755 --- a/syntax/PPConstr.v +++ b/syntax/PPConstr.v @@ -51,6 +51,10 @@ Syntax constr | instantiation_one [ << (CONTEXT $a) >> ] -> [ $a ] | instantiation_many [ << (CONTEXT $a $b ($LIST $l)) >> ] -> [ (CONTEXT $b ($LIST $l)) ";" $a ] + | qualid [ << (QUALID $id ($LIST $l)) >> ] -> [ $id (FIELDS ($LIST $l)) ] + | fieldsnil [ << (FIELDS) >> ] -> [ ] + | fieldscons [ << (FIELDS $id ($LIST $l)) >> ] -> + [ "." $id (FIELDS ($LIST $l)) ] ; (* Things parsed in command1 *) |