From e7d592ada2d681876d2bcf0a45d4267b3746064f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 14 Feb 2001 15:41:55 +0000
Subject: Mise en place d'un système optionnel de discharge immédiat; prise en
 compte des défs locales dans les arguments des inductifs; nettoyage divers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declarations.mli | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index aca6605672..531a616baf 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -17,7 +17,7 @@ type constant_body = {
   const_kind : path_kind;
   const_body : constr option;
   const_type : types;
-  const_hyps : named_context; (* New: younger hyp at top *)
+  const_hyps : section_context; (* New: younger hyp at top *)
   const_constraints : constraints;
   mutable const_opaque : bool }
 
@@ -61,12 +61,13 @@ type one_inductive_body = {
   mind_kelim : sorts list;
   mind_listrec : (recarg list) array;
   mind_finite : bool;
-  mind_nparams : int }
+  mind_nparams : int;
+  mind_params_ctxt : rel_context }
 
 type mutual_inductive_body = {
   mind_kind : path_kind;
   mind_ntypes : int;
-  mind_hyps : named_context;
+  mind_hyps : section_context;
   mind_packets : one_inductive_body array;
   mind_constraints : constraints;
   mind_singl : constr option }
-- 
cgit v1.2.3