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.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'pretyping/program.ml')

diff --git a/pretyping/program.ml b/pretyping/program.ml
index 1bc31646dd..5b9c17d6b2 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -11,12 +11,11 @@
 open CErrors
 open Util
 
-let papp evdref r args =
+let papp sigma r args =
   let open EConstr in
   let gr = delayed_force r in
-  let evd, hd = Evarutil.new_global !evdref gr in
-  evdref := evd;
-  mkApp (hd, args)
+  let evd, hd = Evarutil.new_global sigma gr in
+  sigma, mkApp (hd, args)
 
 let sig_typ   () = Coqlib.lib_ref "core.sig.type"
 let sig_intro () = Coqlib.lib_ref "core.sig.intro"
-- 
cgit v1.2.3