aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar whitequark <whitequark@whitequark.org>2018-06-21 02:34:33 +0000
committerGravatar whitequark <whitequark@whitequark.org>2018-06-21 04:54:34 +0000
commit0f6762ac80cc8d1f37918e9e8f0bb39692979630 (patch)
tree32f739968a88e9fd72feafce02c8d306c7944ec2 /pretyping
parent38c62ef2e9ce28370cd22aadab9d676ffb2bac56 (diff)
Rename Dyn.TParam→ValueS, Dyn.MapS.obj→value to clarify their purpose.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/geninterp.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli
index fa522e9c3..606a6ebea 100644
--- a/pretyping/geninterp.mli
+++ b/pretyping/geninterp.mli
@@ -42,8 +42,8 @@ sig
end
-module ValTMap (M : Dyn.TParam) :
- Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ
+module ValTMap (Value : Dyn.ValueS) :
+ Dyn.MapS with type 'a key = 'a Val.typ and type 'a value = 'a Value.t
(** Dynamic types for toplevel values. While the generic types permit to relate
objects at various levels of interpretation, toplevel values are wearing