diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-18 20:39:08 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 19:23:41 +0100 |
| commit | 00860c1b2209159fb2b6780004c8c8ea16b3cb3a (patch) | |
| tree | 20045d21798206cf742a4bd86668da41cef6e5cf /proofs/proof_global.ml | |
| parent | 34d85e1e899f8a045659ccc53bfd6a1f5104130b (diff) | |
In close_proof only check univ decls with the restricted context.
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index bfd64e21b..cf5dc95fe 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -330,7 +330,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in - let univctx = UState.check_univ_decl ~poly universes universe_decl in let binders = if poly then Some (UState.universe_binders universes) else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to @@ -375,6 +374,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fun t p -> Future.split2 (Future.chain p (make_body t)) else fun t p -> + (* Already checked the univ_decl for the type universes when starting the proof. *) + let univctx = Entries.Monomorphic_const_entry (UState.context_set universes) in Future.from_val (univctx, nf t), Future.chain p (fun (pt,eff) -> (* Deferred proof, we already checked the universe declaration with |