From 891a8a9f7ea3bb5b0b07dc5a2df51314135d8b53 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 23 May 2016 18:58:01 +0200
Subject: Extraction/Projections: Fix bug #4710

Use the compatibility match construction to extract the compatibility
constant associated to a primitive projection.
---
 plugins/extraction/extraction.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 667721e670..bdf01e73b6 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -974,7 +974,10 @@ let extract_constant env kn cb =
     | (Info,TypeScheme) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
-	  | Def c -> mk_typ (Mod_subst.force_constr c)
+	  | Def c ->
+	     (match cb.const_proj with
+	      | None -> mk_typ (Mod_subst.force_constr c)
+	      | Some pb -> mk_typ pb.proj_body)
 	  | OpaqueDef c ->
 	    add_opaque r;
 	    if access_opaque () then
@@ -983,7 +986,10 @@ let extract_constant env kn cb =
     | (Info,Default) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_ax ()
-	  | Def c -> mk_def (Mod_subst.force_constr c)
+	  | Def c ->
+	     (match cb.const_proj with
+	      | None -> mk_def (Mod_subst.force_constr c)
+	      | Some pb -> mk_def pb.proj_body)
 	  | OpaqueDef c ->
 	    add_opaque r;
 	    if access_opaque () then
-- 
cgit v1.2.3