aboutsummaryrefslogtreecommitdiff
path: root/API/API.mllib
diff options
context:
space:
mode:
authorMaxime Dénès2017-08-16 09:44:28 +0200
committerMaxime Dénès2017-08-16 09:44:28 +0200
commite1264c9f0d50bf8ca09fa7388101daa0b4c29635 (patch)
tree3358d182b655bb2510c1d99872ac733474c9124a /API/API.mllib
parent09b54382e52b572f8c091993309adcc4fea3a093 (diff)
parentcf906af70f5c48cab99bd89047af0b2831850cf1 (diff)
Merge PR #912: Detyping functions are now operating on EConstr.t.
Diffstat (limited to 'API/API.mllib')
0 files changed, 0 insertions, 0 deletions