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 /pretyping/typing.ml | |
| parent | d0667eb4a165c065b0d64069641ca0cd39d62219 (diff) | |
Cache meta access in meta_instance.
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index aeb3873de7..e3e5244a8c 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -33,7 +33,7 @@ let meta_type env evd mv = let ty = try Evd.meta_ftype evd mv with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in - meta_instance env evd ty + meta_instance env (create_meta_instance_subst evd) ty let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in |