diff options
| author | coqbot-app[bot] | 2021-04-23 15:57:15 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-23 15:57:15 +0000 |
| commit | 528f8384dcd817e4e339719a5d99c30d48520a8e (patch) | |
| tree | 6be0c3ad09843aeb7fe9efef7f827bf48af44abb /dev/dynlink.ml | |
| parent | d332bbc3c1118631eb8c935ba61a8d071a90428e (diff) | |
| parent | 9b84b41009e5963b5ebb60938a921c5c16175d55 (diff) | |
Merge PR #14158: Provide a reinit data for Ltac2 notations with entry level 4.
Reviewed-by: JasonGross
Diffstat (limited to 'dev/dynlink.ml')
0 files changed, 0 insertions, 0 deletions