diff options
| author | coqbot-app[bot] | 2021-04-21 17:54:37 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-21 17:54:37 +0000 |
| commit | b8b8c73a4f62a8fb964e82c7c779a1aba3264bf4 (patch) | |
| tree | 1f34a2351075ef3570490b0f8b73c2824520589c /interp/notation_ops.ml | |
| parent | f9996cdaf0b6aee12c5b71432b1edb90dffb569a (diff) | |
| parent | f6e393dae62afbb659eab64a530c0cf39403c495 (diff) | |
Merge PR #14094: Properly pass the Ltac2 notation level to the gramlib API.
Reviewed-by: JasonGross
Ack-by: jfehrle
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions