diff options
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 4a9466f4..01083142 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -658,7 +658,12 @@ let add d e i = match i.evar_body with let remove d e = let undf_evars = EvMap.remove e d.undf_evars in let defn_evars = EvMap.remove e d.defn_evars in - { d with undf_evars; defn_evars; } + let principal_future_goal = match d.principal_future_goal with + | None -> None + | Some e' -> if Evar.equal e e' then None else d.principal_future_goal + in + let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in + { d with undf_evars; defn_evars; principal_future_goal; future_goals } let find d e = try EvMap.find e d.undf_evars @@ -1550,9 +1555,12 @@ let meta_with_name evd id = 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 |