diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-17 16:55:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-17 16:55:19 +0200 |
| commit | 78c8d75e38844cb88c551881112e10728962dc2d (patch) | |
| tree | 742d6c1f6c914450427da2340b7a4f698afb6ea7 /plugins/ltac/g_auto.ml4 | |
| parent | 3229a681eaad0cbf4c2aec7d314d4baf0b96feaf (diff) | |
| parent | d10d62918f29ddaea773dd6b767b72ad0e038214 (diff) | |
Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in `comDefinition`.
Diffstat (limited to 'plugins/ltac/g_auto.ml4')
0 files changed, 0 insertions, 0 deletions