diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-06 07:02:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-06 07:10:28 +0200 |
| commit | 82fe255fa41d22b07cee6ad65253707dbda7ce0b (patch) | |
| tree | 199c2e1bb4854ef94f9e71efade8c39c79ec9ec3 /interp/syntax_def.ml | |
| parent | 8114da3ba8a9b31ffe194e7f7f0239ecc2219b9c (diff) | |
Fixing unexpected "noise" introduced in commit 24d5448c.
A file was introduced by mistake in theories/Logic.
Diffstat (limited to 'interp/syntax_def.ml')
0 files changed, 0 insertions, 0 deletions