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

---
 plugins/extraction/extraction.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 0c4fa7055..6559aeb08 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -599,6 +599,7 @@ let rec extract_term env mle mlt c args =
 	extract_cons_app env mle mlt cp args
     | Proj (p, c) ->
         let term = Retyping.expand_projection env (Evd.from_env env) p (EConstr.of_constr c) [] in
+        let term = EConstr.Unsafe.to_constr term in
 	  extract_term env mle mlt term args
     | Rel n ->
 	(* As soon as the expected [mlt] for the head is known, *)
-- 
cgit v1.2.3