aboutsummaryrefslogtreecommitdiff
path: root/engine/geninterp.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-05-08 18:59:55 +0200
committerPierre-Marie Pédrot2016-05-08 19:59:03 +0200
commitf461e7657cab9917c5b405427ddba3d56f197efb (patch)
tree467ac699f78d0360b05174238aeb1177da892503 /engine/geninterp.ml
parent9fe0471ef0127e9301d0450aacaeb1690abb82ad (diff)
Removing dead code and unused opens.
Diffstat (limited to 'engine/geninterp.ml')
-rw-r--r--engine/geninterp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/geninterp.ml b/engine/geninterp.ml
index 45b0aa2316..cfca95d3e6 100644
--- a/engine/geninterp.ml
+++ b/engine/geninterp.ml
@@ -32,7 +32,7 @@ struct
let repr = ValT.repr
let create = ValT.create
- let rec pr : type a. a typ -> Pp.std_ppcmds = fun t -> Pp.str (repr t)
+ let pr : type a. a typ -> Pp.std_ppcmds = fun t -> Pp.str (repr t)
let typ_list = ValT.create "list"
let typ_opt = ValT.create "option"