aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/genarg.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-01-17 01:34:58 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-01-17 01:42:56 +0100
commit15747cc2aaaeeb5d59ec90cda940c1dc6de01a6a (patch)
treef98f1c1010c76afb354cc7766e0037b6f22290d6 /lib/genarg.ml
parentbe7f6f003ff4318dbe962ec141060a9daf92a80d (diff)
Exporting Genarg implementation in the API.
We can now use the expressivity of GADT to work around historical kludges of generic arguments.
Diffstat (limited to 'lib/genarg.ml')
0 files changed, 0 insertions, 0 deletions