From d6d8229dd8d71cf8cac1d116426bf772a9b8821b Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Fri, 7 Jun 2019 14:16:41 +0200
Subject: Fix typing_flags in the checker

Now all relevant typing_flags are taken in account by the checker.
The different forms of assumptions are now printed by the checker.
---
 kernel/environ.ml  | 3 +++
 kernel/environ.mli | 1 +
 2 files changed, 4 insertions(+)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 1b17e954b7..655094e88b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -216,6 +216,9 @@ let lookup_named_ctxt id ctxt =
 let fold_constants f env acc =
   Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc
 
+let fold_inductives f env acc =
+  Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_inductives acc
+
 (* Global constants *)
 
 let lookup_constant_key kn env =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 6cd4f96645..e6d814ac7d 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -176,6 +176,7 @@ val pop_rel_context : int -> env -> env
 
 (** Useful for printing *)
 val fold_constants : (Constant.t -> Opaqueproof.opaque constant_body -> 'a -> 'a) -> env -> 'a -> 'a
+val fold_inductives : (MutInd.t -> Declarations.mutual_inductive_body -> 'a -> 'a) -> env -> 'a -> 'a
 
 (** {5 Global constants }
   {6 Add entries to global environment } *)
-- 
cgit v1.2.3