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/evarsolve.mli | 32 +++++++++++++++++++-------------
 1 file changed, 19 insertions(+), 13 deletions(-)

(limited to 'pretyping/evarsolve.mli')

diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index b6bdc078..3f05c58c 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -1,15 +1,21 @@
 (************************************************************************)
-(*  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 Term
+open EConstr
 open Evd
 open Environ
 
+type alias
+
+val of_alias : alias -> EConstr.t
+
 type unification_result =
   | Success of evar_map
   | UnifFailure of evar_map * Pretype_errors.unification_error
@@ -18,7 +24,7 @@ val is_success : unification_result -> bool
 
 (** Replace the vars and rels that are aliases to other vars and rels by 
    their representative that is most ancient in the context *)
-val expand_vars_in_term : env -> constr -> constr
+val expand_vars_in_term : env -> evar_map -> constr -> constr
 
 (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
    possibly solving related unification problems, possibly leaving open
@@ -44,7 +50,7 @@ val refresh_universes :
   env -> evar_map -> types -> evar_map * types
 
 val solve_refl : ?can_drop:bool -> conv_fun_bool -> env ->  evar_map ->
-  bool option -> existential_key -> constr array -> constr array -> evar_map
+  bool option -> Evar.t -> constr array -> constr array -> evar_map
 
 val solve_evar_evar : ?force:bool ->
   (env -> evar_map -> bool option -> existential -> constr -> evar_map) ->
@@ -57,15 +63,15 @@ val solve_simple_eqn : conv_fun -> ?choose:bool -> env ->  evar_map ->
 val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result
 
 val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result
-(** @deprecated Alias for [reconsider_unif_constraints] *)
+[@@ocaml.deprecated "Alias for [reconsider_unif_constraints]"]
 
 val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
-  constr -> constr list option
+  constr -> alias list option
 
 val is_unification_pattern : env * int -> evar_map -> constr -> constr list ->
-  constr -> constr list option
+  constr -> alias list option
 
-val solve_pattern_eqn : env -> constr list -> constr -> constr
+val solve_pattern_eqn : env -> evar_map -> alias list -> constr -> constr
 
 val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool
 
@@ -73,10 +79,10 @@ exception IllTypedInstance of env * types * types
 
 (* May raise IllTypedInstance if types are not convertible *)
 val check_evar_instance :
-  evar_map -> existential_key -> constr -> conv_fun -> evar_map
+  evar_map -> Evar.t -> constr -> conv_fun -> evar_map
 
 val remove_instance_local_defs :
-  evar_map -> existential_key -> constr array -> constr list
+  evar_map -> Evar.t -> 'a array -> 'a list
 
 val get_type_of_refresh : 
   ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types
-- 
cgit v1.2.3