diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-09-14 18:35:48 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-09-14 18:41:09 +0200 |
| commit | 2bc88f9a536c3db3c2d4a38a8a0da0500b895c7b (patch) | |
| tree | ce5b0fed1af0fb238a23d6b78a57a9bf2df29bb7 /proofs/pfedit.ml | |
| parent | 490160d25d3caac1d2ea5beebbbebc959b1b3832 (diff) | |
Univs: Add universe binding lists to definitions
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index d024c01ba..c77ab06b9 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -133,7 +133,7 @@ open Decl_kinds let next = let n = ref 0 in fun () -> incr n; !n let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = - let evd = Evd.from_env ~ctx Environ.empty_env in + let evd = Evd.from_ctx ctx in start_proof id goal_kind evd sign typ (fun _ -> ()); try let status = by tac in |