diff options
| author | Emilio Jesus Gallego Arias | 2018-05-07 17:30:21 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-07 17:34:10 +0200 |
| commit | d10d62918f29ddaea773dd6b767b72ad0e038214 (patch) | |
| tree | d7865b23b767207ce757949e9fa5889446329d27 /kernel/type_errors.ml | |
| parent | 6c8b00e47334f60f200256d45a5542fa80ce4b12 (diff) | |
[vernac] taint two out-of-api `to_constr` use in `comDefinition`.
This should fix #7448 and #7265.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions