diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-12-17 13:00:55 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-02-07 17:38:00 +0100 |
| commit | ed9ab22b8c3b2210f479689f46d3e4b2fd4f52df (patch) | |
| tree | 8d82cd66f227abd83ce060dd8e27c93bfb2e43a8 /configure.ml | |
| parent | 9e87e9582ffe68ff549347d4fab37f7514992361 (diff) | |
Add test-suite files for hintdb variables in Ltac.
In particular, this closes bug 2417.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions