(*i $Id$ i*)

(*i*)
open Names
open Term
open Sign
open Evd
open Environ
open Reduction
(*i*)

(*s This modules provides useful functions for unification modulo evars *)

val evar_env : 'a evar_info -> env

val dummy_sort : constr
type evar_constraint = conv_pb * constr * constr
type 'a evar_defs = 'a evar_map ref

val reset_problems : unit -> unit
val add_conv_pb : evar_constraint -> unit

val ise_try : 'a evar_defs -> (unit -> bool) list -> bool
val ise_undefined : 'a evar_defs -> constr -> bool
val has_undefined_isevars : 'a evar_defs -> constr -> bool

val make_evar_instance : env -> constr list

val new_isevar : 'a evar_defs -> env -> constr -> path_kind -> constr

val is_eliminator : constr -> bool
val head_is_embedded_evar : 'a evar_defs -> constr -> bool
val solve_simple_eqn :
  (env -> 'a evar_defs -> conv_pb -> constr -> constr -> bool)
  -> env -> 'a evar_defs -> conv_pb * existential * constr -> bool

(* Value/Type constraints *)

type type_constraint = constr option
type val_constraint = constr option

val empty_tycon : type_constraint
val mk_tycon : constr -> type_constraint
val empty_valcon : val_constraint
val mk_valcon : constr -> val_constraint

val split_tycon :
  Rawterm.loc -> env -> 'a evar_defs -> type_constraint -> 
    type_constraint * type_constraint

val valcon_of_tycon : type_constraint -> val_constraint

(* $Id$ *)