diff options
| author | Gaetan Gilbert | 2017-04-06 16:54:15 +0200 |
|---|---|---|
| committer | Gaetan Gilbert | 2017-04-06 16:54:15 +0200 |
| commit | 236c1cc7c071e23c10f50617f79ad75dca1ee664 (patch) | |
| tree | 5f2f81767cad8a6e762e5fd780790391fa68e186 | |
| parent | 9f188da28f65341f5c5ecd0b3b4f9b447bbc2b15 (diff) | |
Avoid strange shadowing of Pretyping.interp_universe_level_name
| -rw-r--r-- | pretyping/pretyping.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 15a48a6a31..df3857df0d 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -223,7 +223,7 @@ let interp_universe ?loc evd = function (evd', Univ.sup u (Univ.Universe.make l))) (evd, Univ.Universe.type0m) l -let interp_universe_level loc evd = function +let interp_level_info loc evd : Misctypes.level_info -> _ = function | None -> new_univ_level_variable ~loc univ_rigid evd | Some (loc,s) -> interp_universe_level_name evd (loc,s) @@ -464,11 +464,10 @@ let evar_kind_of_term sigma c = (*************************************************************************) (* Main pretyping function *) -let interp_universe_level_name loc evd l = - match l with +let interp_glob_level loc evd : Misctypes.glob_level -> _ = function | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set - | GType s -> interp_universe_level loc evd s + | GType s -> interp_level_info loc evd s let pretype_global loc rigid env evd gr us = let evd, instance = @@ -483,7 +482,7 @@ let pretype_global loc rigid env evd gr us = (str "Universe instance should have length " ++ int len) else let evd, l' = List.fold_left (fun (evd, univs) l -> - let evd, l = interp_universe_level_name loc evd l in + let evd, l = interp_glob_level loc evd l in (evd, l :: univs)) (evd, []) l in if List.exists (fun l -> Univ.Level.is_prop l) l' then |