diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-02-28 15:30:15 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-04-10 17:19:21 +0200 |
commit | 306b45f889f83846b1ab10d3b37d9f3e7817a5db (patch) | |
tree | 0aaf21c4606927f7af784c38ab1da4b25fd9f542 /plugins/ltac/coretactics.ml4 | |
parent | 834530272b9006e28a4b7ba35b1f8f861f51e7ce (diff) |
Do not compute constr matching context if not used.
This mitigates bug #6860.
Diffstat (limited to 'plugins/ltac/coretactics.ml4')
0 files changed, 0 insertions, 0 deletions