aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-04-28 16:15:10 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-04-28 16:40:22 +0200
commit7943b1fade775af48917d54878e65b80217be038 (patch)
tree1ea76a0ca0fb5b9a1c1699842268324cae4c1488 /theories/Classes
parent7bdfa1a4e46acf11d199a07bfca0bc59381874c3 (diff)
Using a more explicit algebraic type for evars of kind "MatchingVar".
A priori considered to be a good programming style.
Diffstat (limited to 'theories/Classes')
0 files changed, 0 insertions, 0 deletions