diff options
author | 2018-05-15 15:13:49 +0200 | |
---|---|---|
committer | 2018-05-15 15:13:49 +0200 | |
commit | 927b3826e645d428ebe3d8c6599c1f9e2bf79d46 (patch) | |
tree | aa664725086b1e9672ecba6620d940ef34619dcc /plugins/ltac/tauto.mli | |
parent | cfed57b021b89018d1bb30c6aa0957299fe35d8d (diff) | |
parent | 357c94b3e42d4422e311799771f9e28249fc3608 (diff) |
Merge PR #7213: Do not compute constr matching context if not used.
Diffstat (limited to 'plugins/ltac/tauto.mli')
0 files changed, 0 insertions, 0 deletions