aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_subst.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/mod_subst.ml')
-rw-r--r--kernel/mod_subst.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 6a7ecc442..bf08841c8 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -553,3 +553,8 @@ let subst_substituted s r =
| LSlazy(s',a) ->
ref (LSlazy(s::s',a))
+(* debug *)
+let repr_substituted r =
+ match !r with
+ | LSval a -> None, a
+ | LSlazy(s,a) -> Some s, a