aboutsummaryrefslogtreecommitdiff
path: root/vernac/classes.ml
diff options
context:
space:
mode:
authorMaxime Dénès2020-06-11 18:51:34 +0200
committerMaxime Dénès2020-08-26 16:38:34 +0200
commit46c0b7ab3653a6f1ef4b40466c2dd130d09136cb (patch)
treeb6937b47990e5f76b3f9a5b0fc8999754334ce26 /vernac/classes.ml
parent4e59a68fd6f2cd3cdf936c10cdbfeb46fc22ca95 (diff)
Move given_up goals to evar_map
Diffstat (limited to 'vernac/classes.ml')
0 files changed, 0 insertions, 0 deletions