diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-01 19:32:27 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-02 19:18:31 +0100 |
| commit | ab2afa67a5b4a8254add3294f52cabaa6c7e80a0 (patch) | |
| tree | cfd08b79c5d19b37114b713d4fda7df53cc8e1fe /pretyping/locusops.ml | |
| parent | c717bf2896fbff9361eeefce965dbbea0af0a9ad (diff) | |
Fixing file destruct.v.
Diffstat (limited to 'pretyping/locusops.ml')
0 files changed, 0 insertions, 0 deletions