From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 pretyping/evarsolve.mli | 74 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 74 insertions(+)
 create mode 100644 pretyping/evarsolve.mli

(limited to 'pretyping/evarsolve.mli')

diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
new file mode 100644
index 00000000..21d97609
--- /dev/null
+++ b/pretyping/evarsolve.mli
@@ -0,0 +1,74 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Term
+open Evd
+open Environ
+
+type unification_result =
+  | Success of evar_map
+  | UnifFailure of evar_map * Pretype_errors.unification_error
+
+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
+
+(** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
+   possibly solving related unification problems, possibly leaving open
+   some problems that cannot be solved in a unique way (except if choose is
+   true); fails if the instance is not valid for the given [ev] *)
+
+type conv_fun =
+  env ->  evar_map -> conv_pb -> constr -> constr -> unification_result
+
+type conv_fun_bool =
+  env ->  evar_map -> conv_pb -> constr -> constr -> bool
+
+val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> 
+  bool option -> existential -> constr -> evar_map
+
+val refresh_universes : ?inferred:bool -> ?onlyalg:bool (* Only algebraic universes *) ->
+  bool option (* direction: true for levels lower than the existing levels *) ->
+  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
+
+val solve_evar_evar : ?force:bool ->
+  (env -> evar_map -> bool option -> existential -> constr -> evar_map) ->
+  conv_fun ->
+  env ->  evar_map -> bool option -> existential -> existential -> evar_map
+
+val solve_simple_eqn : conv_fun -> ?choose:bool -> env ->  evar_map ->
+  bool option * existential * constr -> unification_result
+
+val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result
+
+val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
+  constr -> constr list option
+
+val is_unification_pattern : env * int -> evar_map -> constr -> constr list ->
+  constr -> constr list option
+
+val solve_pattern_eqn : env -> constr list -> constr -> constr
+
+val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool
+
+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
+
+val remove_instance_local_defs :
+  evar_map -> existential_key -> constr array -> constr list
+
+val get_type_of_refresh : 
+  ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types
-- 
cgit v1.2.3