aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-09-26 16:07:08 +0200
committerPierre-Marie Pédrot2018-09-26 16:07:08 +0200
commit4ea1dfb16a26959843b2db6fc398556c17abd682 (patch)
treec6abdf06041752d6239700c57840cc0d3d2a0f4d
parentef231c674c11f2f7f6d87bc45f6b909aca26f0c2 (diff)
Fix votour compilation after #8102.
-rw-r--r--checker/votour.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/checker/votour.ml b/checker/votour.ml
index bc820e23dd..1ea0de456e 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -152,6 +152,7 @@ let rec get_name ?(extra=false) = function
|String -> "string"
|Annot (s,v) -> s^"/"^get_name ~extra v
|Dyn -> "<dynamic>"
+ | Proxy v -> get_name ~extra !v
(** For tuples, its quite handy to display the inner 1st string (if any).
Cf. [structure_body] for instance *)
@@ -255,6 +256,7 @@ let rec get_children v o pos = match v with
| _ -> raise Exit
end
|Fail s -> raise Forbidden
+ | Proxy v -> get_children !v o pos
let get_children v o pos =
try get_children v o pos