diff options
| author | Pierre-Marie Pédrot | 2018-09-26 14:03:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-26 14:03:35 +0200 |
| commit | 871c694e5395e85296f4c61ba4039f04704b20b3 (patch) | |
| tree | 7f61099c11a30aa4fa82810fd7949d5ffb1a7bc4 /plugins | |
| parent | 8292c485bde7911bf8a4d626faf9292ba0016e97 (diff) | |
| parent | 8d1a5297d55eb0cd02695c81f6dea7aef6f62d31 (diff) | |
Merge PR #7309: Made names of existential variables interpretable as Ltac variables.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions