diff options
| author | Maxime Dénès | 2018-03-08 17:14:54 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-08 17:14:54 +0100 |
| commit | 3875a525ee1e075be9f0eb1f17c74726e9f38b43 (patch) | |
| tree | f64a545676d221ee1279dfa92903d44d0509196b /plugins/syntax/string_syntax.ml | |
| parent | e9d2a40ed12e31095565b5c7401f02af997a7cc7 (diff) | |
| parent | a768e75f761ae444c05162ec1d064795d413ba25 (diff) | |
Merge PR #6918: romega: get rid of EConstr.Unsafe
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions