diff options
| author | Emilio Jesus Gallego Arias | 2018-09-06 12:37:41 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-06 13:14:09 +0200 |
| commit | dcb26e0cb3b4860abb4a5bb36d5f77403dabd654 (patch) | |
| tree | eb49556526f767ff595de1801418357a6da1a2c4 | |
| parent | 3af27f47bafb9b9d464de2839c6a425f008d8fc8 (diff) | |
[pfedit] Fix master build due to merge conflict
| -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 b48f14ca82..d971c28a26 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -173,7 +173,7 @@ 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 = UState.merge side_eff Evd.univ_rigid univs ctx in + let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in cb, status, univs let refine_by_tactic env sigma ty tac = |