aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/recordops.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-11-05 21:36:40 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 17:23:53 +0100
commitb7fd585b89ac5e0b7770f52739c33fe179f2eed8 (patch)
tree83ab6fe2ccecb503691c9842ba7eec27690ad975 /pretyping/recordops.mli
parent147afe827dc83602cc160a8b1357e84ecea910ff (diff)
Evarsolve API using EConstr.
Diffstat (limited to 'pretyping/recordops.mli')
0 files changed, 0 insertions, 0 deletions