diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-04 15:42:41 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-04 15:48:32 +0200 |
| commit | 2ac8e0edebe0d9a6bde4d997327dbd2ffcde08b6 (patch) | |
| tree | b144dcb1689899b5135289903932b18de55d9904 /parsing/g_constr.ml4 | |
| parent | 86c6649382bb9e42281ffe956c627c6d3987559b (diff) | |
- Allow parsing of @const@{instance} for specifying universe instances of polymorphic
constants.
Diffstat (limited to 'parsing/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 81645a580..69ba73c67 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -161,7 +161,7 @@ GEXTEND Gram ; constr: [ [ c = operconstr LEVEL "8" -> c - | "@"; f=global -> CAppExpl(!@loc,(None,f,None),[]) ] ] + | "@"; f=global; i = instance -> CAppExpl(!@loc,(None,f,i),[]) ] ] ; operconstr: [ "200" RIGHTA @@ -185,7 +185,7 @@ GEXTEND Gram | "90" RIGHTA [ ] | "10" LEFTA [ f=operconstr; args=LIST1 appl_arg -> CApp(!@loc,(None,f),args) - | "@"; f=global; args=LIST0 NEXT -> CAppExpl(!@loc,(None,f,None),args) + | "@"; f=global; i = instance; args=LIST0 NEXT -> CAppExpl(!@loc,(None,f,i),args) | "@"; (locid,id) = pattern_identref; args=LIST1 identref -> let args = List.map (fun x -> CRef (Ident x,None), None) args in CApp(!@loc,(None,CPatVar(locid,(true,id))),args) ] |