diff options
| author | Pierre-Marie Pédrot | 2015-11-20 11:27:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-20 11:27:45 +0100 |
| commit | f01b73bd6f5a66cde730c584df6be08e06bf2042 (patch) | |
| tree | 294b074f4752fdb39f24ea4e2f55349558e9db26 /engine | |
| parent | 5ccadc40d54090df5e6b61b4ecbb6083d01e5a88 (diff) | |
| parent | 574e510ba069f1747ecb1e5a17cf86c902d79d44 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 7 | ||||
| -rw-r--r-- | engine/evd.mli | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 60239ebfe2..069fcbfa6e 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1096,9 +1096,12 @@ let meta_name evd mv = let clear_metas evd = {evd with metas = Metamap.empty} -let meta_merge evd1 evd2 = +let meta_merge ?(with_univs = true) evd1 evd2 = let metas = Metamap.fold Metamap.add evd1.metas evd2.metas in - let universes = union_evar_universe_context evd2.universes evd1.universes in + let universes = + if with_univs then union_evar_universe_context evd2.universes evd1.universes + else evd2.universes + in {evd2 with universes; metas; } type metabinding = metavariable * constr * instance_status diff --git a/engine/evd.mli b/engine/evd.mli index 25d8a8c3d2..57399f2b5e 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -448,7 +448,7 @@ val meta_reassign : metavariable -> constr * instance_status -> evar_map -> eva val clear_metas : evar_map -> evar_map (** [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *) -val meta_merge : evar_map -> evar_map -> evar_map +val meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map val undefined_metas : evar_map -> metavariable list val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map |