diff options
| author | Hugo Herbelin | 2014-09-18 16:15:34 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-18 16:40:24 +0200 |
| commit | 6d549d3a2b0ab89c77e34646e866584522bd3591 (patch) | |
| tree | 003b5f74bb978949c2a048ad6dfb8015a4c7dcc3 /dev | |
| parent | 870d81c699b5d15420a03f2006a7938a158c09a8 (diff) | |
For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop in Class_tactics).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions