diff options
| author | Enrico Tassi | 2016-06-15 17:58:42 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-06-15 17:58:42 +0200 |
| commit | 2b8596c568e243302bfec7f98e8ff8ca1ec0834a (patch) | |
| tree | f8e9832abd030810ff711adda35fac08fcf1ec1b /kernel/typeops.ml | |
| parent | 7385d3c7fc6b3bd7101e6a7ce5ff00008e187e89 (diff) | |
ssrmatching: ltac argument parsing made more robust
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions
