diff options
| author | Gaëtan Gilbert | 2018-08-23 09:35:21 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-08-28 12:48:46 +0200 |
| commit | e705297921639fa0aef7d6e50e58d50257de3160 (patch) | |
| tree | b2576dd961761620736c820fbb4c39875dc7004d /proofs | |
| parent | f885e8a88620351d9dc4b0969f520d13197f2184 (diff) | |
Fix #7795: UGraph.AlreadyDeclared with Program
This change is based on noticing that we use a default value for the
`sideff` argument even though we have a similarly named `side_eff`
available. Someone who knows how side effects and universes are
supposed to interact should check this.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 678c3ea3f7..b48f14ca82 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -173,8 +173,8 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = const_entry_body = Future.chain ce.const_entry_body (fun (pt, _) -> pt, ()) } in let (cb, ctx), () = Future.force ce.const_entry_body in - let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in - cb, status, Evd.evar_universe_context univs' + let univs = UState.merge side_eff Evd.univ_rigid univs ctx in + cb, status, univs let refine_by_tactic env sigma ty tac = (** Save the initial side-effects to restore them afterwards. We set the |