diff options
| author | Matthieu Sozeau | 2015-09-14 18:35:48 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-09-14 18:41:09 +0200 |
| commit | 2bc88f9a536c3db3c2d4a38a8a0da0500b895c7b (patch) | |
| tree | ce5b0fed1af0fb238a23d6b78a57a9bf2df29bb7 /proofs | |
| 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')
| -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 d024c01ba5..c77ab06b94 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 |