From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 02:12:40 +0100
Subject: Evar-normalizing functions now act on EConstrs.

---
 pretyping/coercion.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'pretyping/coercion.ml')

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index ead44cee2f..91f53a886d 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -417,7 +417,6 @@ let inh_tosort_force loc env evd j =
   try
     let t,p = lookup_path_to_sort_from env evd j.uj_type in
     let evd,j1 = apply_coercion env evd p j t in
-    let whd_evar evd c = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr c)) in
     let j2 = on_judgment_type (whd_evar evd) j1 in
       (evd,type_judgment env evd j2)
   with Not_found | NoCoercion ->
-- 
cgit v1.2.3