diff options
| author | Pierre-Marie Pédrot | 2015-10-09 10:31:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-09 10:31:13 +0200 |
| commit | eb7da0d0a02a406c196214ec9d08384385541788 (patch) | |
| tree | efe031d7df32573abd7b39afa0f009a6d61f18d5 /engine/evd.ml | |
| parent | 84add29c036735ceacde73ea98a9a5a454a5e3a0 (diff) | |
| parent | 73daf37ccc7a44cd29c9b67405111756c75cb26a (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 13 |
1 files changed, 3 insertions, 10 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 3f4bfe7afe..64aad80821 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1021,8 +1021,8 @@ let merge_uctx sideff rigid uctx ctx' = let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial } -let merge_context_set rigid evd ctx' = - {evd with universes = merge_uctx false rigid evd.universes ctx'} +let merge_context_set ?(sideff=false) rigid evd ctx' = + {evd with universes = merge_uctx sideff rigid evd.universes ctx'} let merge_uctx_subst uctx s = { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } @@ -1067,12 +1067,6 @@ let uctx_new_univ_variable rigid name predicative uctx_univ_algebraic = Univ.LSet.add u avars}, false else {uctx with uctx_univ_variables = uvars'}, false in - (* let ctx' = *) - (* if pred then *) - (* Univ.ContextSet.add_constraints *) - (* (Univ.Constraint.singleton (Univ.Level.set, Univ.Le, u)) ctx' *) - (* else ctx' *) - (* in *) let names = match name with | Some n -> add_uctx_names n u uctx.uctx_names @@ -1323,8 +1317,7 @@ let normalize_evar_universe_context uctx = Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic in - if Univ.LSet.equal (fst us') (fst uctx.uctx_local) then - uctx + if Univ.ContextSet.equal us' uctx.uctx_local then uctx else let us', universes = Universes.refresh_constraints uctx.uctx_initial_universes us' in let uctx' = |