diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-02-27 13:43:06 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-02-27 13:43:06 +0100 |
| commit | 5bd9452721495296cf4f2f34c77bc27e16377e8e (patch) | |
| tree | 5804199c41da779c7e6103f9e235baaf82118563 /configure.ml | |
| parent | 04d086e21cdf28c4029133a0f8fd1720d13544e8 (diff) | |
| parent | ed9ab22b8c3b2210f479689f46d3e4b2fd4f52df (diff) | |
Merge PR#395: Allow hintdb to be parameters in a Ltac definition or
Tactic Notation
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions