diff options
| author | Gaëtan Gilbert | 2018-08-28 15:19:13 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-13 15:05:57 +0200 |
| commit | cc66d4a0977db4994000bfc7e45937b3ccff3c93 (patch) | |
| tree | d7ef363064917a10b895793a67006ded5775b98b | |
| parent | 230f135eb7ba80b4be74da493f205a7eb1b5fa3d (diff) | |
Avoid repeat universe declarations for constants with split univs
| -rw-r--r-- | kernel/term_typing.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 43351737e5..f59e07098b 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -256,6 +256,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let tyj = infer_type env typ in let proofterm = Future.chain body (fun ((body,uctx),side_eff) -> + (* don't redeclare universes which are declared for the type *) + let uctx = Univ.ContextSet.diff uctx univs in let j, uctx = match trust with | Pure -> let env = push_context_set uctx env in |