aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/coercion.ml8
-rw-r--r--pretyping/typing.mli4
2 files changed, 9 insertions, 3 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index ea8557b18..c9c2445a7 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -197,7 +197,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
(subst1 hdy restT') (succ i) (fun x -> eq_app (co x))
else Some (fun x ->
let term = co x in
- Typing.e_solve_evars env evdref term)
+ let sigma, term = Typing.solve_evars env !evdref term in
+ evdref := sigma; term)
in
if isEvar !evdref c || isEvar !evdref c' || not (Program.is_program_generalized_coercion ()) then
(* Second-order unification needed. *)
@@ -343,8 +344,9 @@ let app_coercion env evdref coercion v =
match coercion with
| None -> v
| Some f ->
- let v' = Typing.e_solve_evars env evdref (f v) in
- whd_betaiota !evdref v'
+ let sigma, v' = Typing.solve_evars env !evdref (f v) in
+ evdref := sigma;
+ whd_betaiota !evdref v'
let coerce_itf ?loc env evd v t c1 =
let evdref = ref evd in
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index da05102f2..3cf43ace0 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -26,14 +26,17 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
(** Variant of [type_of] using references instead of state-passing. *)
val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
+[@@ocaml.deprecated "Use [Typing.type_of]"]
(** Typecheck a type and return its sort *)
val sort_of : env -> evar_map -> types -> evar_map * Sorts.t
val e_sort_of : env -> evar_map ref -> types -> Sorts.t
+[@@ocaml.deprecated "Use [Typing.sort_of]"]
(** Typecheck a term has a given type (assuming the type is OK) *)
val check : env -> evar_map -> constr -> types -> evar_map
val e_check : env -> evar_map ref -> constr -> types -> unit
+[@@ocaml.deprecated "Use [Typing.check]"]
(** Returns the instantiated type of a metavariable *)
val meta_type : evar_map -> metavariable -> types
@@ -41,6 +44,7 @@ val meta_type : evar_map -> metavariable -> types
(** Solve existential variables using typing *)
val solve_evars : env -> evar_map -> constr -> evar_map * constr
val e_solve_evars : env -> evar_map ref -> constr -> constr
+[@@ocaml.deprecated "Use [Typing.solve_evars]"]
(** Raise an error message if incorrect elimination for this inductive *)
(** (first constr is term to match, second is return predicate) *)