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.

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

(limited to 'pretyping/patternops.ml')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index d473f41bdf..ffd6e73faa 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -163,7 +163,7 @@ let pattern_of_constr env sigma t =
     | Ind (sp,u)    -> PRef (canonical_gr (IndRef sp))
     | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp))
     | Proj (p, c) -> 
-      pattern_of_constr env (EConstr.of_constr (Retyping.expand_projection env sigma p c []))
+      pattern_of_constr env (Retyping.expand_projection env sigma p c [])
     | Evar (evk,ctxt as ev) ->
       (match snd (Evd.evar_source evk sigma) with
       | Evar_kinds.MatchingVar (b,id) ->
-- 
cgit v1.2.3