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 /intf/decl_kinds.ml | |
parent | e29948c5606bfcab182cf0f325750fdb3215856e (diff) |
Typo in comment in tactic_matching.ml.
Diffstat (limited to 'intf/decl_kinds.ml')
0 files changed, 0 insertions, 0 deletions