diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-15 16:05:27 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-15 16:05:27 +0000 |
commit | d3097cd34ffffda5dbe332ee88fd33d54180fad9 (patch) | |
tree | b634215effd11bfa01b25750522c441013a2ced2 /checker/votour.ml | |
parent | 4bd2e928e3b8d463bb793ad814ff42abdabf9611 (diff) |
Checker: vo validation checks the absence of Var/Evar/Meta
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16405 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/votour.ml')
-rw-r--r-- | checker/votour.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/checker/votour.ml b/checker/votour.ml index 19c188310..4e8729033 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -14,6 +14,7 @@ open Values let rec get_name ?(extra=false) = function |Any -> "?" + |Fail -> assert false |Tuple (name,_) -> name |Sum (name,_,_) -> name |Array v -> "array"^(if extra then "/"^get_name ~extra v else "") @@ -79,6 +80,7 @@ let rec get_children v o pos = match v with if Obj.is_block o && Obj.tag o < Obj.no_scan_tag then Array.init (Obj.size o) (fun i -> (Any,Obj.field o i,i::pos)) else [||] + |Fail -> assert false type info = { nam : string; |