diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-30 13:01:48 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-10 18:27:28 +0100 |
| commit | 8c59f1a464a446191f48358fe2484ec65ac0ef1c (patch) | |
| tree | 85701335471ba6a62bc267d01747fc26c5e5c665 /checker/votour.ml | |
| parent | d439c01190f45de5ac493b8f55d361503e83ad03 (diff) | |
Add interfaces for checker and remove dead code.
Diffstat (limited to 'checker/votour.ml')
| -rw-r--r-- | checker/votour.ml | 6 |
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"^ |