diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-02-14 11:36:04 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-02-14 11:36:04 +0100 |
commit | 4fd59386e7f60d16bfe9858c372b354d422ac0b6 (patch) | |
tree | 9f8bd1216d3943b2202804ab92334f11edf7df99 /vernac/auto_ind_decl.ml | |
parent | b85742f187ec4d87733f88587534772502ad9a7d (diff) | |
parent | 7ce9edaeb49520990efb6785627cc1d6c80f7be6 (diff) |
Merge PR#253: Sort Search results by relevance
Diffstat (limited to 'vernac/auto_ind_decl.ml')
0 files changed, 0 insertions, 0 deletions