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

(limited to 'pretyping/pretyping.ml')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6b6800ac6a..4660978df3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -143,9 +143,6 @@ let nf_fix sigma (nas, cs, ts) =
   let inj c = EConstr.to_constr sigma c in
   (nas, Array.map inj cs, Array.map inj ts)
 
-let nf_evar sigma c =
-  EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr c))
-
 let search_guard loc env possible_indexes fixdefs =
   (* Standard situation with only one possibility for each fix. *)
   (* We treat it separately in order to get proper error msg. *)
-- 
cgit v1.2.3