From 66139b2e1f66b826dd5dbdb8a9ade64a4d5e11c6 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 15 Apr 2013 16:05:03 +0000
Subject: Checker: empty sections hardcoded in cb and mind

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16400 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/term.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'checker/term.ml')

diff --git a/checker/term.ml b/checker/term.ml
index b52f08cfa..a3c9225f5 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -209,6 +209,9 @@ let subst1 lam = substl [lam]
 (*     Type of assumptions and contexts                                    *)
 (***************************************************************************)
 
+type named_declaration = Id.t * constr option * constr
+type named_context = named_declaration list
+
 let empty_named_context = []
 let fold_named_context f l ~init = List.fold_right f l init
 
-- 
cgit v1.2.3