diff options
| author | Hugo Herbelin | 2019-09-25 19:24:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-09-25 19:24:35 +0200 |
| commit | 59079a232d2157c0c4bea4cb1a3cd68c9410e880 (patch) | |
| tree | e5cbf8cdb687eb9d629621845bf5f7b978fc487c /kernel/section.ml | |
| parent | 227fcc4dff6fbb68ad6b91387b2f36705329a57e (diff) | |
| parent | beeb3ed57c4749ff84524250a8b79dfa0b1e2f78 (diff) | |
Merge PR #10713: Define morphisms of real numbers and accelerate Cauchy reals
Reviewed-by: herbelin
Diffstat (limited to 'kernel/section.ml')
0 files changed, 0 insertions, 0 deletions