diff options
author | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-09-01 16:22:52 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-07-03 13:39:18 +0200 |
commit | bff2278b7e558a58cb322edfb301c6241adf379b (patch) | |
tree | c0ace3604b43a79d9dc8b044d0a0f103468c9d27 /engine/univSubst.ml | |
parent | cea3d7c83bf3aae18262e62b897ec204c098e444 (diff) |
Remove unused output of Universes.normalize_univ_variables
Diffstat (limited to 'engine/univSubst.ml')
-rw-r--r-- | engine/univSubst.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/engine/univSubst.ml b/engine/univSubst.ml index 6a433d9fb..2f59a3fa8 100644 --- a/engine/univSubst.ml +++ b/engine/univSubst.ml @@ -162,13 +162,13 @@ let subst_opt_univs_constr s = let normalize_univ_variables ctx = let ctx = normalize_opt_subst ctx in - let undef, def, subst = - Univ.LMap.fold (fun u v (undef, def, subst) -> + let def, subst = + Univ.LMap.fold (fun u v (def, subst) -> match v with - | None -> (Univ.LSet.add u undef, def, subst) - | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst)) - ctx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty) - in ctx, undef, def, subst + | None -> (def, subst) + | Some b -> (Univ.LSet.add u def, Univ.LMap.add u b subst)) + ctx (Univ.LSet.empty, Univ.LMap.empty) + in ctx, def, subst let pr_universe_body = function | None -> mt () |