From d3097cd34ffffda5dbe332ee88fd33d54180fad9 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 15 Apr 2013 16:05:27 +0000
Subject: 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
---
 checker/votour.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'checker/votour.ml')

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;
-- 
cgit v1.2.3