diff options
| author | Pierre-Marie Pédrot | 2021-04-20 10:16:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-04-20 10:16:55 +0200 |
| commit | b36fb9f68884090e5b06f9837da084395f519f96 (patch) | |
| tree | f969092affe593d2220a015b5a712ff934ba72bd /plugins/extraction/mlutil.ml | |
| parent | c3d7754ec2045a964974698821adb73c586b4e41 (diff) | |
| parent | 1dffce05d5b7b26a890a9d0359e54946e661511b (diff) | |
Merge PR #14089: unify for Ltac2
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/extraction/mlutil.ml')
0 files changed, 0 insertions, 0 deletions