diff options
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 |