From c3e26fca1d077a2b69926df85d05e067882c40b0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 19 Dec 2017 08:33:55 +0100
Subject: Specific type for section definition entries.

This allows to statically ensure well-formedness properties.
---
 kernel/term_typing.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/term_typing.mli')

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index c771452a19..4b893b0564 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -18,7 +18,7 @@ type _ trust =
 | Pure : unit trust
 | SideEffects : structure_body -> side_effects trust
 
-val translate_local_def : env -> Id.t -> unit definition_entry ->
+val translate_local_def : env -> Id.t -> section_def_entry ->
   constant_def * types * Univ.ContextSet.t
 
 val translate_local_assum : env -> types -> types
-- 
cgit v1.2.3