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

---
 plugins/funind/functional_principles_types.mli | 28 +++++++++++---------------
 1 file changed, 12 insertions(+), 16 deletions(-)

(limited to 'plugins/funind/functional_principles_types.mli')

diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 3fa2644c..33aeafef 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -1,14 +1,15 @@
 (************************************************************************)
-(*  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 Misctypes
+open Constr
 
 val generate_functional_principle :
   Evd.evar_map ref -> 
@@ -17,7 +18,7 @@ val generate_functional_principle :
   (* induction principle on rel *)
   types ->
   (* *)
-  sorts array option ->
+  Sorts.t array option ->
   (* Name of the new principle *)
   (Id.t) option ->
   (* the compute functions to use   *)
@@ -27,18 +28,13 @@ val generate_functional_principle :
   (* The tactic to use to make the proof w.r
      the number of params
   *)
-  (constr array -> int -> Tacmach.tactic) ->
+  (EConstr.constr array -> int -> Tacmach.tactic) ->
   unit
 
-val compute_new_princ_type_from_rel : constr array -> sorts array ->
-  types -> types
-
-
 exception No_graph_found
 
 val make_scheme :   Evd.evar_map ref ->
- (pconstant*glob_sort) list -> Safe_typing.private_constants Entries.definition_entry list
-
-val build_scheme : (Id.t*Libnames.reference*glob_sort) list ->  unit
-val build_case_scheme : (Id.t*Libnames.reference*glob_sort)  ->  unit
+ (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list
 
+val build_scheme : (Id.t*Libnames.reference*Sorts.family) list ->  unit
+val build_case_scheme : (Id.t*Libnames.reference*Sorts.family)  ->  unit
-- 
cgit v1.2.3