diff options
| author | Matthieu Sozeau | 2014-04-01 19:19:22 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:58 +0200 |
| commit | a2fce6d14d00a437466a1f7e3b53a77229f87980 (patch) | |
| tree | 2e88133b978c67c222f0bfd7c13416609cdc84ac /pretyping | |
| parent | 4d7956a9b3f7f44aa9dae1bf22258b12dacab65f (diff) | |
- Fix eq_constr_universes restricted to Sorts.equal
- Fix passing of universe contexts through definitions/proofs, abstract is ok now, even
in presence of polymorphism
- Correctly mark unresolvable the evars made by the Simple abstraction.
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 = |