diff options
| author | Pierre-Marie Pédrot | 2019-11-07 14:29:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-07 14:29:05 +0100 |
| commit | 64ddd9ac0c34e560a0640297e2e23b6aaf074810 (patch) | |
| tree | 7b590829827e08609be9595d4cae86c82e8aff0f /dev | |
| parent | 5c5831e35747f25d8aeadf10a13cd60e9b7adfbb (diff) | |
| parent | 3b257c35c0b0e85fcbae0cdc4c93d124003a6464 (diff) | |
Merge PR #11049: Prevent redefinition of Ltac2 types and constructors inside a module
Reviewed-by: ppedrot
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions