diff options
| author | Hugo Herbelin | 2020-10-31 13:23:05 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-04 16:56:49 +0100 |
| commit | 404a041fce68b4f7072de0b91b4e136f04250482 (patch) | |
| tree | da2cc1f6f2cde4839bb7796147ef9260fa4ba183 /engine/evd.ml | |
| parent | 11cb6dd5f4a719db6926ff0d99a72fbdbbf2d8bf (diff) | |
Cosmetic cleaning of uState.ml and related: a bit of doc, more unity in naming.
Also some dead code.
If no typo is introduced, there should be no semantic changes.
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 4ae1d034d7..0fb32e5150 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -834,7 +834,7 @@ let empty = { let from_env e = { empty with universes = UState.from_env e } -let from_ctx ctx = { empty with universes = ctx } +let from_ctx uctx = { empty with universes = uctx } let has_undefined evd = not (EvMap.is_empty evd.undf_evars) |