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 /checker/term.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 'checker/term.ml')
| -rw-r--r-- | checker/term.ml | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/checker/term.ml b/checker/term.ml index 3372f9b6c..e8cdb03e9 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -397,16 +397,6 @@ let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *) (* Universe substitutions *) -let subst_univs_puniverses subst = - if Univ.is_empty_level_subst subst then fun c -> c - else - let f = Univ.Instance.subst subst in - fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u') - -let subst_univs_fn_puniverses fn = - let f = Univ.Instance.subst_fn fn in - fun ((c, u) as x) -> let u' = f u in if u' == u then x else (c, u') - let map_constr f c = map_constr_with_binders (fun x -> x) (fun _ c -> f c) 0 c let subst_univs_fn_constr f c = |