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/evarconv.mli | 26 +++++++++++++++-----------
 1 file changed, 15 insertions(+), 11 deletions(-)

(limited to 'pretyping/evarconv.mli')

diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 2231e5bc..9270d6e3 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -1,13 +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 EConstr
 open Environ
 open Reductionops
 open Evd
@@ -36,7 +38,7 @@ val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -
 val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map
 
 val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map
-(** @deprecated Alias for [solve_unif_constraints_with_heuristics] *)
+[@@ocaml.deprecated "Alias for [solve_unif_constraints_with_heuristics]"]
 
 (** Check all pending unification problems are solved and raise an
     error otherwise *)
@@ -46,18 +48,18 @@ val check_problems_are_solved : env -> evar_map -> unit
 (** Check if a canonical structure is applicable *)
 
 val check_conv_record : env -> evar_map -> 
-  constr * types Stack.t -> constr * types Stack.t ->
-  Univ.universe_context_set * (constr * constr) 
+  state -> state ->
+  Univ.ContextSet.t * (constr * constr) 
   * constr * constr list * (constr Stack.t * constr Stack.t) *
-    (constr Stack.t * types Stack.t) *
-    (constr Stack.t * types Stack.t) * constr *
+    (constr Stack.t * constr Stack.t) *
+    (constr Stack.t * constr Stack.t) * constr *
     (int option * constr)
 
 (** Try to solve problems of the form ?x[args] = c by second-order
     matching, using typing to select occurrences *)
 
 val second_order_matching : transparent_state -> env -> evar_map ->
-  existential -> occurrences option list -> constr -> evar_map * bool
+  EConstr.existential -> occurrences option list -> constr -> evar_map * bool
 
 (** Declare function to enforce evars resolution by using typing constraints *)
 
@@ -80,3 +82,5 @@ val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * bool ->
       Evarsolve.unification_result
 (**/**)
 
+(** {6 Functions to deal with impossible cases } *)
+val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set
-- 
cgit v1.2.3