aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/votour.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/votour.ml')
-rw-r--r--checker/votour.ml6
1 files changed, 2 insertions, 4 deletions
diff --git a/checker/votour.ml b/checker/votour.ml
index 77c9999c4..8cb97a2b1 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -210,7 +210,6 @@ let access_list v o pos =
let access_block o = match Repr.repr o with
| BLOCK (tag, os) -> (tag, os)
| _ -> raise Exit
-let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit
(** raises Exit if the object has not the expected structure *)
exception Forbidden
@@ -249,8 +248,7 @@ let rec get_children v o pos = match v with
|Dyn ->
begin match Repr.repr o with
| BLOCK (0, [|id; o|]) ->
- let n = access_int id in
- let tpe = find_dyn n in
+ let tpe = Any in
[|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|]
| _ -> raise Exit
end
@@ -395,7 +393,7 @@ let visit_vo f =
| None -> ()
done
-let main =
+let () =
if not !Sys.interactive then
Arg.parse [] visit_vo
("votour: guided tour of a Coq .vo or .vi file\n"^