aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/impargs.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-04-13 12:00:55 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-04-13 12:03:34 +0200
commitf0f3d650ec4fcd1644811e099f0f3f50d660a992 (patch)
treee4a99885401e799e1e578430daf1ab2bb51e5d16 /library/impargs.ml
parentd78784bd86d3d571bb2891356e9e9718c69976ba (diff)
parentd632f64403da813e240973a9caf06c79e262a7ec (diff)
Uniformizing the semantics of ARGUMENT EXTEND macros.
Most notably, we bring the single argument and three argument variants closer, so that the various TYPED AS clauses may be optional. Compile-time warnings have been added for redundant clauses.
Diffstat (limited to 'library/impargs.ml')
0 files changed, 0 insertions, 0 deletions