diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-06-20 21:58:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-24 11:14:14 +0200 |
| commit | 1b3b1b36cfd21f3f79b7aec7249acc8ab292f25a (patch) | |
| tree | 8fc5a9c26a29e07e6e0e9006e1d0574fab807ee8 /plugins/extraction/extract_env.ml | |
| parent | e29948c5606bfcab182cf0f325750fdb3215856e (diff) | |
Typo in comment in tactic_matching.ml.
Diffstat (limited to 'plugins/extraction/extract_env.ml')
0 files changed, 0 insertions, 0 deletions