diff options
| author | Matej Kosik | 2015-10-29 10:27:51 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:08 +0100 |
| commit | 05276561ebff16d434b475b9e80586194619a832 (patch) | |
| tree | f3008641f84db3968bfc566e165d09c105ae1892 /kernel/declareops.ml | |
| parent | 950dace27c3233f740b2031c9d99cb3f155aefbf (diff) | |
ENH: the concept of the 'algebraic universe' was added to the 'Global Index'.
Diffstat (limited to 'kernel/declareops.ml')
0 files changed, 0 insertions, 0 deletions