diff options
| author | Matthieu Sozeau | 2014-05-02 11:34:53 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:59:01 +0200 |
| commit | 2de8910d2cc0af096e6d91b0ea165997ce144503 (patch) | |
| tree | 1e2345eea549fdc176f7abe17123a0be3051289b /proofs | |
| parent | ce11f55e27c8e4f98384aacd61ee67c593340195 (diff) | |
- Fix treatment of global universe constraints which should be passed along
in the Evd of proofs (Evd.from_env).
- Allow to set the Store.t value of new evars, e.g. to set constraint evars as
unresolvable in rewrite.ml.
- Fix a HUGE performance problem in the processing of constraints, which was remerging
all the previous constraints with the ambient global universes at each new constraint addition.
Performance is now back to (or better than) normal.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index e49a57af39..5cb677d1c6 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -226,7 +226,7 @@ let start_proof id str goals terminator = let initial_state = { pid = id; terminator = Ephemeron.create terminator; - proof = Proof.start Evd.empty goals; + proof = Proof.start (Evd.from_env (Global.env ())) goals; endline_tactic = None; section_vars = None; strength = str; @@ -237,7 +237,7 @@ let start_dependent_proof id str goals terminator = let initial_state = { pid = id; terminator = Ephemeron.create terminator; - proof = Proof.dependent_start Evd.empty goals; + proof = Proof.dependent_start (Evd.from_env (Global.env ())) goals; endline_tactic = None; section_vars = None; strength = str; |