diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 6 | ||||
| -rw-r--r-- | pretyping/evd.mli | 1 | ||||
| -rw-r--r-- | pretyping/unification.ml | 1 |
3 files changed, 8 insertions, 0 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index eda5f66c1c..d185685005 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -932,6 +932,12 @@ let merge_uctx rigid uctx ctx' = let merge_context_set rigid evd ctx' = {evd with universes = merge_uctx rigid evd.universes ctx'} +let merge_uctx_subst uctx s = + { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } + +let merge_universe_subst evd subst = + {evd with universes = merge_uctx_subst evd.universes subst } + let with_context_set rigid d (a, ctx) = (merge_context_set rigid d ctx, a) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 9be18bc8ae..5cc554c26a 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -469,6 +469,7 @@ val universes : evar_map -> Univ.universes val merge_universe_context : evar_map -> evar_universe_context -> evar_map val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map +val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 9e662150ee..0ab886ca30 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -384,6 +384,7 @@ let is_rigid_head flags t = match kind_of_term t with | Const (cst,u) -> not (Cpred.mem cst (snd flags.modulo_delta)) | Ind (i,u) -> true + | Fix _ | CoFix _ -> true | _ -> false let force_eqs c = |