aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/pp.mli
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-03-17 18:44:23 +0100
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-03-17 18:44:23 +0100
commitadb721441e9ff9bf7cdb1b4603628d95ca1f016a (patch)
treeda10d09179338729799ba253c6ac2e30b8dfbaf5 /lib/pp.mli
parent4d95eb4e878f375a69f1b48d8833801bf555fdd0 (diff)
Add function to fix the non-substituted universe variables of an evar_map.
Diffstat (limited to 'lib/pp.mli')
0 files changed, 0 insertions, 0 deletions