diff options
| author | Pierre-Marie Pédrot | 2015-06-30 16:39:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-07-03 04:16:31 +0200 |
| commit | 31c7542731a62f56bd60f443a84d68813f8780a8 (patch) | |
| tree | 869635fac06174b40babe4acc047ec621db5b79a /kernel | |
| parent | 6482ca75a39709e65de676d533b3d115ad2b1153 (diff) | |
Fixing bug #4265: coqdep does not handle From ... Require.
The search algorithm is not satisfactory though, as it crawls through
all known files to find the proper one. We should rather use some trie-based
data structure, but I'll leave this for a future commit.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions