diff options
| author | coqbot-app[bot] | 2021-03-23 20:38:58 +0000 |
|---|---|---|
| committer | GitHub | 2021-03-23 20:38:58 +0000 |
| commit | 285d5e03a230af7b327cba0b7720217ede664761 (patch) | |
| tree | d8f3bcac6bce50f5235e5416c7504b1b722a7848 /plugins | |
| parent | d3f78cad1532f000106ed0c0b8be2ac384ce1d3a (diff) | |
| parent | 01b061f0082a70f66016e78075a5952af8ed5431 (diff) | |
Merge PR #13978: Do not match on record types with mutable fields in function arguments.
Reviewed-by: gares
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index da4a50b674..cfdaac710b 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -217,13 +217,13 @@ module Mlenv = struct (* Adding a type with no [Tvar], hence no generalization needed. *) - let push_type {env=e;free=f} t = - { env = (0,t) :: e; free = find_free f t} + let push_type mle t = + { env = (0,t) :: mle.env; free = find_free mle.free t} (* Adding a type with no [Tvar] nor [Tmeta]. *) - let push_std_type {env=e;free=f} t = - { env = (0,t) :: e; free = f} + let push_std_type mle t = + { env = (0,t) :: mle.env; free = mle.free} end |