From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 pretyping/indrec.mli | 35 +++++++++++++++++++----------------
 1 file changed, 19 insertions(+), 16 deletions(-)

(limited to 'pretyping/indrec.mli')

diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 192b64a5..7a68443b 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -1,20 +1,22 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Environ
 open Evd
 
 (** Errors related to recursors building *)
 
 type recursion_scheme_error =
-  | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive
+  | NotAllowedCaseAnalysis of (*isrec:*) bool * Sorts.t * pinductive
   | NotMutualInScheme of inductive * inductive
   | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive
 
@@ -26,26 +28,27 @@ type dep_flag = bool
 
 (** Build a case analysis elimination scheme in some sort family *)
 
-val build_case_analysis_scheme : env -> 'r Sigma.t -> pinductive ->
-      dep_flag -> sorts_family -> (constr, 'r) Sigma.sigma
+val build_case_analysis_scheme : env -> Evd.evar_map -> pinductive ->
+      dep_flag -> Sorts.family -> evar_map * Constr.t
 
 (** Build a dependent case elimination predicate unless type is in Prop
    or is a recursive record with primitive projections. *)
 
-val build_case_analysis_scheme_default : env -> 'r Sigma.t -> pinductive ->
-      sorts_family -> (constr, 'r) Sigma.sigma
+val build_case_analysis_scheme_default : env -> evar_map -> pinductive ->
+      Sorts.family -> evar_map * Constr.t
 
 (** Builds a recursive induction scheme (Peano-induction style) in the same
    sort family as the inductive family; it is dependent if not in Prop
    or a recursive record with primitive projections.  *)
 
 val build_induction_scheme : env -> evar_map -> pinductive ->
-      dep_flag -> sorts_family -> evar_map * constr
+      dep_flag -> Sorts.family -> evar_map * constr
 
 (** Builds mutual (recursive) induction schemes *)
 
 val build_mutual_induction_scheme :
-  env -> evar_map -> (pinductive * dep_flag * sorts_family) list -> evar_map * constr list
+  env -> evar_map -> ?force_mutual:bool ->
+  (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list
 
 (** Scheme combinators *)
 
@@ -54,13 +57,13 @@ val build_mutual_induction_scheme :
    scheme quantified on sort [s]. [set] asks for [s] be declared equal to [i],
   otherwise just less or equal to [i]. *)
 
-val weaken_sort_scheme : env -> evar_map -> bool -> sorts -> int -> constr -> types -> 
+val weaken_sort_scheme : env -> evar_map -> bool -> Sorts.t -> int -> constr -> types ->
   evar_map * types * constr
 
 (** Recursor names utilities *)
 
-val lookup_eliminator : inductive -> sorts_family -> Globnames.global_reference
-val elimination_suffix : sorts_family -> string
-val make_elimination_ident : Id.t -> sorts_family -> Id.t
+val lookup_eliminator : inductive -> Sorts.family -> Globnames.global_reference
+val elimination_suffix : Sorts.family -> string
+val make_elimination_ident : Id.t -> Sorts.family -> Id.t
 
 val case_suffix : string
-- 
cgit v1.2.3