From 3264fdaa71b2327a992286a08df0dfbcf78ea4fe Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 7 Jul 2015 17:31:04 +0200
Subject: Checker: Fix bug #4282

Adapt to new [projection] abstract type comprising a constant and
a boolean.
---
 checker/values.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'checker/values.ml')

diff --git a/checker/values.ml b/checker/values.ml
index b2d74821d4..46b66adc4a 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 f5fd749af797e08efee22122742bc740 checker/cic.mli
+MD5 cabb12868c5ab7a51dbc6dc2ae8c0894 checker/cic.mli
 
 *)
 
@@ -126,6 +126,7 @@ let v_caseinfo =
   v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
 
 let v_cast = v_enum "cast_kind" 4
+let v_proj = v_tuple "projection" [|v_cst; v_bool|]
 
 let rec v_constr =
   Sum ("constr",0,[|
@@ -145,7 +146,7 @@ let rec v_constr =
     [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *)
     [|v_fix|]; (* Fix *)
     [|v_cofix|]; (* CoFix *)
-    [|v_cst;v_constr|] (* Proj *)
+    [|v_proj;v_constr|] (* Proj *)
   |])
 
 and v_prec = Tuple ("prec_declaration",
@@ -205,8 +206,10 @@ let v_cst_def =
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
 
 let v_projbody =
-  v_tuple "projection_body" [|v_cst;Int;Int;v_constr;v_tuple "proj_eta" [|v_constr;v_constr|];
-			      v_constr|]
+  v_tuple "projection_body"
+	  [|v_cst;Int;Int;v_constr;
+	    v_tuple "proj_eta" [|v_constr;v_constr|];
+	    v_constr|]
 
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
-- 
cgit v1.2.3


From 9c732a5c878bac2592cb397aca3d17cfefdcd023 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 Jul 2015 01:13:59 +0200
Subject: Option -type-in-type: added support in checker and making it
 contaminating in vo files (this was not done yet in 24d0027f0 and
 090fffa57b).

Reused field "engagement" to carry information about both
impredicativity of set and type in type.

For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
---
 checker/values.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'checker/values.ml')

diff --git a/checker/values.ml b/checker/values.ml
index 46b66adc4a..e82ba10327 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -193,7 +193,9 @@ let v_lazy_constr =
 
 (** kernel/declarations *)
 
-let v_engagement = v_enum "eng" 1
+let v_impredicative_set = v_enum "impr-set" 2
+let v_type_in_type = v_enum "type-in-type" 2
+let v_engagement = v_tuple "eng" [|v_impredicative_set; v_type_in_type|]
 
 let v_pol_arity =
   v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
@@ -315,7 +317,7 @@ and v_modtype =
 let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
 let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
 let v_compiled_lib =
-  v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|]
+  v_tuple "compiled" [|v_dp;v_module;v_deps;v_engagement;Any|]
 
 (** Library objects *)
 
-- 
cgit v1.2.3


From b3f8288b2243efe59d3358ad4001dd78d62308b8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 11 Jul 2015 23:59:32 +0200
Subject: Updating checksum in checker (9c732a5cc continued).

Calling md5sum test earlier, at the time coqchk is built, rather than
at testing time, hopefully moving it closer to what it is supposed to
occur.
---
 checker/values.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/values.ml')

diff --git a/checker/values.ml b/checker/values.ml
index e82ba10327..45220bd051 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 cabb12868c5ab7a51dbc6dc2ae8c0894 checker/cic.mli
+MD5 8b7e75b4b94a2d8506a62508e0374c0a checker/cic.mli
 
 *)
 
-- 
cgit v1.2.3