From 536026f3e20f761e8ef366ed732da7d3b626ac5e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 15:39:01 +0100
Subject: Cleaning up opening of the EConstr module in pretyping folder.

---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2cb9e08648..eebb2a0380 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3165,7 +3165,7 @@ let expand_projections env sigma c =
   let sigma = Sigma.to_evar_map sigma in
   let rec aux env c =
     match EConstr.kind sigma c with
-    | Proj (p, c) -> EConstr.of_constr (Retyping.expand_projection env sigma p (aux env c) [])
+    | Proj (p, c) -> Retyping.expand_projection env sigma p (aux env c) []
     | _ -> map_constr_with_full_binders sigma push_rel aux env c
   in
   EConstr.Unsafe.to_constr (aux env (EConstr.of_constr c))
-- 
cgit v1.2.3