diff options
| author | Pierre-Marie Pédrot | 2020-07-02 15:55:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-12 14:07:13 +0200 |
| commit | 2423629321d46c7facc59b4206bbb773725ec63d (patch) | |
| tree | 6fc338fae07cd10969f587de02868d92bc0712bb /plugins/syntax | |
| parent | e52a8a898352f55fb544e2b563c81fd1247c8130 (diff) | |
Do not tamper with hints in Class_tactics.with_prods.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions