diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-17 01:34:58 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-17 01:42:56 +0100 |
commit | 15747cc2aaaeeb5d59ec90cda940c1dc6de01a6a (patch) | |
tree | f98f1c1010c76afb354cc7766e0037b6f22290d6 /lib/genarg.ml | |
parent | be7f6f003ff4318dbe962ec141060a9daf92a80d (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