diff options
| author | coqbot-app[bot] | 2020-12-18 15:52:16 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-18 15:52:16 +0000 |
| commit | 82d0a578b91f4de87deebc658b0e085646ca63d4 (patch) | |
| tree | 0319a8f8f880d8d4585c04062560067fda039f3b /pretyping/typing.ml | |
| parent | 8013852eb0957141181110a904aeff7b37a8219d (diff) | |
| parent | 7a8761b0ca9c503592c14ee98402e530cde28846 (diff) | |
Merge PR #13628: Cache meta instances in Clenv
Reviewed-by: mattam82
Reviewed-by: gares
Ack-by: SkySkimmer
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 |