From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 toplevel/ind_tables.mli | 24 +++++++++++++-----------
 1 file changed, 13 insertions(+), 11 deletions(-)

(limited to 'toplevel/ind_tables.mli')

diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index 3cb3541e..98eaac09 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,10 +8,6 @@
 
 open Term
 open Names
-open Libnames
-open Mod_subst
-open Sign
-open Declarations
 
 (** This module provides support for registering inductive scheme builders,
    declaring schemes and generating schemes on demand *)
@@ -22,8 +18,10 @@ type mutual
 type individual
 type 'a scheme_kind
 
-type mutual_scheme_object_function = mutual_inductive -> constr array
-type individual_scheme_object_function = inductive -> constr
+type mutual_scheme_object_function =
+  mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects
+type individual_scheme_object_function =
+  inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects
 
 (** Main functions to register a scheme builder *)
 
@@ -31,7 +29,8 @@ val declare_mutual_scheme_object : string -> ?aux:string ->
   mutual_scheme_object_function -> mutual scheme_kind
 
 val declare_individual_scheme_object : string -> ?aux:string ->
-  individual_scheme_object_function -> individual scheme_kind
+  individual_scheme_object_function ->
+  individual scheme_kind
 
 (*
 val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit
@@ -41,12 +40,15 @@ val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit
 
 val define_individual_scheme : individual scheme_kind -> 
   Declare.internal_flag (** internal *) ->
-  identifier option -> inductive -> constant
+  Id.t option -> inductive -> constant * Declareops.side_effects
 
 val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) ->
-  (int * identifier) list -> mutual_inductive -> constant array
+  (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects
 
 (** Main function to retrieve a scheme in the cache or to generate it *)
-val find_scheme : 'a scheme_kind -> inductive -> constant
+val find_scheme : 'a scheme_kind -> inductive -> constant * Declareops.side_effects
 
 val check_scheme : 'a scheme_kind -> inductive -> bool
+
+
+val pr_scheme_kind : 'a scheme_kind -> Pp.std_ppcmds
-- 
cgit v1.2.3