From 83e0cb59ed9a07bdf0154aaa2169bc94acf88c19 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 27 Mar 2018 02:37:19 +0200
Subject: Swapping Context and Constr: defining declarations on constr in
 Constr.

This shall eventually allow to use contexts of declarations in the
definition of the "Case" constructor.

Basically, this means that Constr now includes Context and that the
"t" types of Context which were specialized on constr are not defined
in Constr (unfortunately using a heavy boilerplate).
---
 library/lib.mli | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'library/lib.mli')

diff --git a/library/lib.mli b/library/lib.mli
index 1d77212e9d..5abfccfc7d 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Names
+
 (** Lib: record of operations, backtrack, low-level sections *)
 
 (** This module provides a general mechanism to keep a trace of all operations
@@ -153,7 +154,7 @@ val unfreeze : frozen -> unit
 val init : unit -> unit
 
 (** {6 Section management for discharge } *)
-type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
+type variable_info = Constr.named_declaration * Decl_kinds.binding_kind
 type variable_context = variable_info list 
 type abstr_info = private {
   abstr_ctx : variable_context;
@@ -165,7 +166,7 @@ type abstr_info = private {
 }
 
 val instance_from_variable_context : variable_context -> Id.t array
-val named_of_variable_context : variable_context -> Context.Named.t
+val named_of_variable_context : variable_context -> Constr.named_context
 
 val section_segment_of_constant : Constant.t -> abstr_info
 val section_segment_of_mutual_inductive: MutInd.t -> abstr_info
@@ -179,9 +180,9 @@ val is_in_section : GlobRef.t -> bool
 val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit
 val add_section_context : Univ.ContextSet.t -> unit
 val add_section_constant : Decl_kinds.polymorphic ->
-  Constant.t -> Context.Named.t -> unit
+  Constant.t -> Constr.named_context -> unit
 val add_section_kn : Decl_kinds.polymorphic ->
-  MutInd.t -> Context.Named.t -> unit
+  MutInd.t -> Constr.named_context -> unit
 val replacement_context : unit -> Opaqueproof.work_list
 
 (** {6 Discharge: decrease the section level if in the current section } *)
-- 
cgit v1.2.3