From 943e6b23229b5eed2fb8265089563ce0a25b9b44 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 29 Apr 2013 16:02:46 +0000
Subject: Merging Context and Sign.

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

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 5d9eaa9284..24572da591 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -47,7 +47,7 @@ type native_name =
   | NotLinked
 
 type constant_body = {
-    const_hyps : Sign.section_context; (** New: younger hyp at top *)
+    const_hyps : Context.section_context; (** New: younger hyp at top *)
     const_body : constant_def;
     const_type : constant_type;
     const_body_code : Cemitcodes.to_patch_substituted;
@@ -132,7 +132,7 @@ type mutual_inductive_body = {
 
     mind_ntypes : int;  (** Number of types in the block *)
 
-    mind_hyps : Sign.section_context;  (** Section hypotheses on which the block depends *)
+    mind_hyps : Context.section_context;  (** Section hypotheses on which the block depends *)
 
     mind_nparams : int;  (** Number of expected parameters *)
 
-- 
cgit v1.2.3