diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-03 10:57:46 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-03 10:57:46 +0100 |
| commit | 87f3278ea3520ed2b2a4b355765392550488c1df (patch) | |
| tree | aaef8759f8f2755a4194c5de370ab3fc3325c25d /engine | |
| parent | 97e82c1a520382ec34cfedcc55b5190126b05703 (diff) | |
| parent | d073a70d84aa6802a03d03a17d2246d607e85db1 (diff) | |
Merge PR #6047: A generic printer for ltac values
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/geninterp.ml | 2 | ||||
| -rw-r--r-- | engine/geninterp.mli | 4 |
2 files changed, 6 insertions, 0 deletions
diff --git a/engine/geninterp.ml b/engine/geninterp.ml index e79e258fb..2a1addcd3 100644 --- a/engine/geninterp.ml +++ b/engine/geninterp.ml @@ -47,6 +47,8 @@ struct end +module ValTMap = ValT.Map + module ValReprObj = struct type ('raw, 'glb, 'top) obj = 'top Val.tag diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 492e372ad..ae0b26e59 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -39,6 +39,10 @@ sig val inject : 'a tag -> 'a -> t end + +module ValTMap (M : Dyn.TParam) : + Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ + (** Dynamic types for toplevel values. While the generic types permit to relate objects at various levels of interpretation, toplevel values are wearing their own type regardless of where they came from. This allows to use the |