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

---
 kernel/typeops.mli | 60 +++++++++++++++++-------------------------------------
 1 file changed, 19 insertions(+), 41 deletions(-)

(limited to 'kernel/typeops.mli')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 2112284e..85b2cfff 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -1,21 +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 Constr
 open Univ
-open Term
 open Environ
 open Entries
-open Declarations
 
 (** {6 Typing functions (not yet tagged as safe) }
 
-    They return unsafe judgments that are "in context" of a set of 
+    They return unsafe judgments that are "in context" of a set of
     (local) universe variables (the ones that appear in the term)
     and associated constraints. In case of polymorphic definitions,
     these variables and constraints will be generalized.
@@ -38,27 +39,28 @@ val assumption_of_judgment :  env -> unsafe_judgment -> types
 val type_judgment          :  env -> unsafe_judgment -> unsafe_type_judgment
 
 (** {6 Type of sorts. } *)
+val type1 : types
+val type_of_sort : Sorts.t -> types
 val judge_of_prop : unsafe_judgment
 val judge_of_set  : unsafe_judgment
-val judge_of_prop_contents  : contents -> unsafe_judgment
-val judge_of_type           : universe -> unsafe_judgment
+val judge_of_prop_contents  : Sorts.contents -> unsafe_judgment
+val judge_of_type           : Universe.t -> unsafe_judgment
 
 (** {6 Type of a bound variable. } *)
+val type_of_relative : env -> int -> types
 val judge_of_relative : env -> int -> unsafe_judgment
 
 (** {6 Type of variables } *)
+val type_of_variable : env -> variable -> types
 val judge_of_variable : env -> variable -> unsafe_judgment
 
 (** {6 type of a constant } *)
 
 val judge_of_constant : env -> pconstant -> unsafe_judgment
 
-val judge_of_constant_knowing_parameters :
-  env -> pconstant -> types Lazy.t array -> unsafe_judgment
-
 (** {6 type of an applied projection } *)
 
-val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment
+val judge_of_projection : env -> Projection.t -> unsafe_judgment -> unsafe_judgment
 
 (** {6 Type of application. } *)
 val judge_of_apply :
@@ -70,9 +72,9 @@ val judge_of_abstraction :
   env -> Name.t -> unsafe_type_judgment -> unsafe_judgment
     -> unsafe_judgment
 
-val sort_of_product : env -> sorts -> sorts -> sorts
-
 (** {6 Type of a product. } *)
+val sort_of_product : env -> Sorts.t -> Sorts.t -> Sorts.t
+val type_of_product : env -> Name.t -> Sorts.t -> Sorts.t -> types
 val judge_of_product :
   env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment
     -> unsafe_judgment
@@ -91,9 +93,6 @@ val judge_of_cast :
 
 val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment
 
-(* val judge_of_inductive_knowing_parameters : *)
-(*   env -> inductive -> unsafe_judgment array -> unsafe_judgment *)
-
 val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment
 
 (** {6 Type of Cases. } *)
@@ -101,30 +100,9 @@ val judge_of_case : env -> case_info
   -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
     -> unsafe_judgment
 
-(** Typecheck general fixpoint (not checking guard conditions) *)
-val type_fixpoint : env -> Name.t array -> types array
-    -> unsafe_judgment array -> unit
-
-val type_of_constant : env -> pconstant -> types constrained
-
-val type_of_constant_type : env -> constant_type -> types
-
-val type_of_projection : env -> Names.projection puniverses -> types
+val type_of_projection_constant : env -> Projection.t puniverses -> types
 
 val type_of_constant_in : env -> pconstant -> types
 
-val type_of_constant_type_knowing_parameters :
-  env -> constant_type -> types Lazy.t array -> types
-
-val type_of_constant_knowing_parameters :
-  env -> pconstant -> types Lazy.t array -> types constrained
-
-val type_of_constant_knowing_parameters_in :
-  env -> pconstant -> types Lazy.t array -> types
-
-(** Make a type polymorphic if an arity *)
-val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
-  constant_type
-
 (** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> constr -> Context.section_context -> unit
+val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit
-- 
cgit v1.2.3