diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-04 23:30:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-05 22:57:42 +0200 |
| commit | fd8357fad3f4d608f62afce848a4d4bf1bbb3d70 (patch) | |
| tree | 602b3de0176f68127cef981d7df8a4a462f58570 | |
| parent | bc7bea8fd028e12b1d3199128c788af671176af7 (diff) | |
Small code simplification.
| -rw-r--r-- | library/universes.ml | 11 | ||||
| -rw-r--r-- | pretyping/evd.ml | 8 |
2 files changed, 7 insertions, 12 deletions
diff --git a/library/universes.ml b/library/universes.ml index c5363fd9a..b6c891c2f 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -505,7 +505,8 @@ let subst_univs_fn_puniverses lsubst (c, u as cu) = let u' = Instance.subst_fn lsubst u in if u' == u then cu else (c, u') -let nf_evars_and_universes_gen f subst = +let nf_evars_and_universes_opt_subst f subst = + let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in let lsubst = Univ.level_subst_of subst in let rec aux c = match kind_of_term c with @@ -528,10 +529,6 @@ let nf_evars_and_universes_gen f subst = | _ -> map_constr aux c in aux -let nf_evars_and_universes_opt_subst f subst = - let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in - nf_evars_and_universes_gen f subst - let fresh_universe_context_set_instance ctx = if ContextSet.is_empty ctx then LMap.empty, ctx else @@ -788,9 +785,7 @@ let normalize_context_set ctx us algs = (* Noneqs is now in canonical form w.r.t. equality constraints, and contains only inequality constraints. *) let noneqs = subst_univs_level_constraints subst noneqs in - let us = - LMap.subst_union (LMap.map (fun v -> Some (Universe.make v)) subst) us - in + let us = LMap.fold (fun u v acc -> LMap.add u (Some (Universe.make v)) acc) subst us in (* Compute the left and right set of flexible variables, constraints mentionning other variables remain in noneqs. *) let noneqs, ucstrsl, ucstrsr = diff --git a/pretyping/evd.ml b/pretyping/evd.ml index a003716f9..cd02d7228 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -959,12 +959,12 @@ let merge_uctx rigid uctx ctx' = match rigid with | UnivRigid -> uctx | UnivFlexible b -> - let uvars' = Univ.LMap.subst_union uctx.uctx_univ_variables - (Univ.LMap.bind (fun _ -> None) (Univ.ContextSet.levels ctx')) in + let levels = Univ.ContextSet.levels ctx' in + let uvars' = Univ.LMap.bind (fun _ -> None) levels in + let uvars' = Univ.LMap.fold Univ.LMap.add uctx.uctx_univ_variables uvars' in if b then { uctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = Univ.LSet.union uctx.uctx_univ_algebraic - (Univ.ContextSet.levels ctx') } + uctx_univ_algebraic = Univ.LSet.union uctx.uctx_univ_algebraic levels } else { uctx with uctx_univ_variables = uvars' } in { uctx with uctx_local = Univ.ContextSet.union uctx.uctx_local ctx'; |