diff options
| author | Pierre-Marie Pédrot | 2020-04-04 17:04:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-14 09:54:46 +0100 |
| commit | 981146bbc716494ba9ced0d6b403923b293cdec1 (patch) | |
| tree | dd74ec6343737c31e7a00acd3779a5bff9a5527c /proofs | |
| parent | d0667eb4a165c065b0d64069641ca0cd39d62219 (diff) | |
Cache meta access in meta_instance.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 387f0f6f5f..f47ed0fc4b 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -42,10 +42,10 @@ type clausenv = { let cl_env ce = ce.env let cl_sigma ce = ce.evd -let clenv_term clenv c = meta_instance clenv.env clenv.evd c +let clenv_term clenv c = meta_instance clenv.env (create_meta_instance_subst clenv.evd) c let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv -let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval -let clenv_type clenv = meta_instance clenv.env clenv.evd clenv.templtyp +let clenv_value clenv = meta_instance clenv.env (create_meta_instance_subst clenv.evd) clenv.templval +let clenv_type clenv = meta_instance clenv.env (create_meta_instance_subst clenv.evd) clenv.templtyp let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t @@ -203,7 +203,7 @@ let clenv_assign mv rhs clenv = *) let clenv_metas_in_type_of_meta env evd mv = - (mk_freelisted (meta_instance env evd (meta_ftype evd mv))).freemetas + (mk_freelisted (meta_instance env (create_meta_instance_subst evd) (meta_ftype evd mv))).freemetas let dependent_in_type_of_metas clenv mvs = List.fold_right |