diff options
| author | coqbot-app[bot] | 2021-04-20 20:55:51 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-20 20:55:51 +0000 |
| commit | 3645c06030ed1266fd4160ec7211b4447731bf13 (patch) | |
| tree | f3ee437a6f9ace297c0be6ade2cd4aae1a4b09a5 /interp/implicit_quantifiers.ml | |
| parent | cab7a5ddb906e5cef57d78ba7435e89354f3125b (diff) | |
| parent | 9d3ea20fb8e9f1c3acfa3d127a1e3ee99fe7ebc9 (diff) | |
Merge PR #14133: Slightly tweak the not-unit Ltac2 warning.
Reviewed-by: JasonGross
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions