diff options
| author | Hugo Herbelin | 2017-04-28 16:15:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-31 02:04:10 +0200 |
| commit | bf3b52f6a950490ad99b032cb0b41d32cff64824 (patch) | |
| tree | f880e1ce1989cd67c06c8a29284f35fc123bec09 /kernel/nativecode.ml | |
| parent | 5dd98189c6554733fe4e22401e1637330cc8a30a (diff) | |
Using a more explicit algebraic type for evars of kind "MatchingVar".
A priori considered to be a good programming style.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions