From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 pretyping/pretyping.mli | 27 +++++++++++++++++++--------
 1 file changed, 19 insertions(+), 8 deletions(-)

(limited to 'pretyping/pretyping.mli')

diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index ac899a78..0f3f7c3c 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -29,7 +29,7 @@ type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
 type var_map = Pattern.constr_under_binders Id.Map.t
 type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
-type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t
+type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
 
 type ltac_var_map = {
   ltac_constrs : var_map;
@@ -47,14 +47,19 @@ val empty_lvar : ltac_var_map
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
 
+type inference_hook = env -> evar_map -> evar -> evar_map * constr
+
 type inference_flags = {
   use_typeclasses : bool;
-  use_unif_heuristics : bool;
-  use_hook : (env -> evar_map -> evar -> constr) option;
+  solve_unification_constraints : bool;
+  use_hook : inference_hook option;
   fail_evar : bool;
   expand_evars : bool
 }
 
+type 'a delayed_open =
+  { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
+
 val default_inference_flags : bool -> inference_flags
 
 val no_classes_no_fail_inference_flags : inference_flags
@@ -114,6 +119,11 @@ val understand_judgment : env -> evar_map ->
 val understand_judgment_tcc : env -> evar_map ref ->
   glob_constr -> unsafe_judgment
 
+val type_uconstr :
+  ?flags:inference_flags ->
+  ?expected_type:typing_constraint ->
+  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr delayed_open
+
 (** Trying to solve remaining evars and remaining conversion problems
     possibly using type classes, heuristics, external tactic solver
     hook depending on given flags. *)
@@ -130,6 +140,10 @@ val solve_remaining_evars : inference_flags ->
 val check_evars_are_solved :
   env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit
 
+(** [check_evars env initial_sigma extended_sigma c] fails if some
+   new unresolved evar remains in [c] *)
+val check_evars : env -> evar_map -> evar_map -> constr -> unit
+
 (**/**)
 (** Internal of Pretyping... *)
 val pretype :
@@ -148,12 +162,9 @@ val ise_pretype_gen :
 
 (** To embed constr in glob_constr *)
 
-val constr_in : constr -> Dyn.t
-val constr_out : Dyn.t -> constr
-
-val interp_sort : evar_map -> glob_sort -> evar_map * sorts
+val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts
 val interp_elimination_sort : glob_sort -> sorts_family
 
 val genarg_interp_hook :
-  (types -> env -> evar_map -> Genarg.typed_generic_argument Id.Map.t ->
+  (types -> env -> evar_map -> unbound_ltac_var_map ->
     Genarg.glob_generic_argument -> constr * evar_map) Hook.t
-- 
cgit v1.2.3