From d079ec262eacc2149fa46b45ac23097a3333b5fe Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 15 Nov 2018 13:30:26 +0100
Subject: More informative error on vo validation failure

Now that the checker shares code with the kernel using md5 cic.mli
doesn't work. We could md5 declarations.ml but this would miss changes
to constr (and cic.mli already missed changes to names, univs).

Instead we just print a bit of information (the last seen type
name/annotation) when validate fails. This should help debugging when
forgetting to update values.ml without the full verbosity of -debug.

As such there is no need to -debug in the makefile validate
target (NB: CI has an independent implementation of the validate rule
since the vos are installed there).
---
 checker/values.mli | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

(limited to 'checker/values.mli')

diff --git a/checker/values.mli b/checker/values.mli
index 1b1437a469..616b69907f 100644
--- a/checker/values.mli
+++ b/checker/values.mli
@@ -10,17 +10,36 @@
 
 type value =
   | Any
+  (** A value that we won't check, *)
+
   | Fail of string
+  (** A value that shouldn't be there at all, *)
+
   | Tuple of string * value array
+  (** A debug name and sub-values in this block *)
+
   | Sum of string * int * value array array
+  (** A debug name, a number of constant constructors, and sub-values
+     at each position of each possible constructed variant *)
+
   | Array of value
   | List of value
   | Opt of value
   | Int
   | String
+  (** Builtin Ocaml types. *)
+
   | Annot of string * value
+  (** Adds a debug note to the inner value *)
+
   | Dyn
+  (** Coq's Dyn.t *)
+
   | Proxy of value ref
+  (** Same as the inner value, used to define recursive types *)
+
+(** NB: List and Opt have their own constructors to make it easy to
+   define eg [let rec foo = List foo]. *)
 
 val v_univopaques : value
 val v_libsum : value
-- 
cgit v1.2.3