diff options
| author | Pierre-Marie Pédrot | 2021-03-25 13:20:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-25 13:20:24 +0100 |
| commit | d328a04d5e533a8591dfb3f2fa3d0e0852037f33 (patch) | |
| tree | 581ad378661d135d18c90c790ff4abb30e54c1f3 /interp/notation_ops.ml | |
| parent | fa27883cf87c564cc82133cabdcb71b9cc2dd3ad (diff) | |
| parent | 1657b1156c29d969f1e8a1b5785e17d5984ea7a6 (diff) | |
Merge PR #13989: fix documentation of Ltac2.Env.expand
Reviewed-by: JasonGross
Reviewed-by: ppedrot
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions