aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses_errors.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-11-06 21:59:18 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 17:26:38 +0100
commitb77579ac873975a15978c5a4ecf312d577746d26 (patch)
tree772e41667e74c38582ff6f4645c73e7d7556f935 /pretyping/typeclasses_errors.mli
parent258c8502eafd3e078a5c7478a452432b5c046f71 (diff)
Tacred API using EConstr.
Diffstat (limited to 'pretyping/typeclasses_errors.mli')
0 files changed, 0 insertions, 0 deletions