diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-21 18:31:41 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-21 18:41:37 +0200 |
| commit | 2b7ccb235b503f4c978009c2d7908d305cf85925 (patch) | |
| tree | ad3c4a3d218c20318c70fdd261edddcafbaf8b19 /library/universes.ml | |
| parent | 99efd521c3bd01f885248f6ac03c450e98929b2e (diff) | |
Cleanup substitution inside universe instances, only done through subst_fn now,
and disable hashconsing of substituted instances which had a huge performance
penalty in general. They are hashconsed when put in the environment only now.
Diffstat (limited to 'library/universes.ml')
| -rw-r--r-- | library/universes.ml | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/library/universes.ml b/library/universes.ml index 1c704bc22..788af000b 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -508,32 +508,6 @@ let choose_canonical ctx flexible algs s = let canon = LSet.choose algs in canon, (global, rigid, LSet.remove canon flexible) -let subst_puniverses subst (c, u as cu) = - let u' = Instance.subst subst u in - if u' == u then cu else (c, u') - -let nf_evars_and_universes_local f subst = - let rec aux c = - match kind_of_term c with - | Evar (evdk, _ as ev) -> - (match f ev with - | None -> c - | Some c -> aux c) - | Const pu -> - let pu' = subst_puniverses subst pu in - if pu' == pu then c else mkConstU pu' - | Ind pu -> - let pu' = subst_puniverses subst pu in - if pu' == pu then c else mkIndU pu' - | Construct pu -> - let pu' = subst_puniverses subst pu in - if pu' == pu then c else mkConstructU pu' - | Sort (Type u) -> - let u' = Univ.subst_univs_level_universe subst u in - if u' == u then c else mkSort (sort_of_univ u') - | _ -> map_constr aux c - in aux - 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') |