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/cases.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'pretyping/cases.ml')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index cbd04a76ad..fbca1c5f0d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2126,11 +2126,6 @@ let eq_id avoid id =
   let hid' = next_ident_away hid avoid in
     hid'
 
-let papp sigma gr args =
-  let evdref = ref sigma in
-  let ans = papp evdref gr args in
-  !evdref, ans
-
 let mk_eq sigma typ x y = papp sigma coq_eq_ind [| typ; x ; y |]
 let mk_eq_refl sigma typ x = papp sigma coq_eq_refl [| typ; x |]
 let mk_JMeq sigma typ x typ' y =
-- 
cgit v1.2.3