From 3ad5a919dd266da3775660b29e0b387519e6e04a Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 22 May 2019 00:29:47 +0200
Subject: Remove `unsafe_type_of` from `Coercion`

We thread explicitly the evar map everywhere for this purpose.
---
 pretyping/program.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping/program.mli')

diff --git a/pretyping/program.mli b/pretyping/program.mli
index 6604b3a854..7da0da1297 100644
--- a/pretyping/program.mli
+++ b/pretyping/program.mli
@@ -10,6 +10,7 @@
 
 open Names
 open EConstr
+open Evd
 
 (** A bunch of Coq constants used by Program *)
 
@@ -38,7 +39,7 @@ val mk_coq_and : Evd.evar_map -> constr list -> Evd.evar_map * constr
 val mk_coq_not : Evd.evar_map -> constr -> Evd.evar_map * constr
 
 (** Polymorphic application of delayed references *)
-val papp : Evd.evar_map ref -> (unit -> GlobRef.t) -> constr array -> constr
+val papp : evar_map -> (unit -> GlobRef.t) -> constr array -> evar_map * constr
 
 val get_proofs_transparency : unit -> bool
 val is_program_cases : unit -> bool
-- 
cgit v1.2.3