From 984890d972aaa0586b509058dc4fcea5f2c3ca2d Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 25 Aug 2011 16:54:51 +0000
Subject: Extraction: allow extraction of records with anonymous fields (fix
 #2555)

 For Ocaml, we now use the extraction-reserved substring "__" :
 The name foo__i will be pick for i-th field of record foo if it is anonymous.

 For Haskell, still no printing of records as native records,
 hence nothing to do.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14420 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/table.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'plugins/extraction/table.ml')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index c58672ca0a..502d062353 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -362,10 +362,6 @@ let error_MPfile_as_mod mp b =
 	    "Monolithic Extraction cannot deal with this situation.\n"^
 	    "Please "^s2^"use (Recursive) Extraction Library instead.\n"))
 
-let error_record r =
-  err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++
-       fnl () ++ str "To help extraction, please use an explicit name.")
-
 let msg_non_implicit r n id =
   let name = match id with
     | Anonymous -> ""
-- 
cgit v1.2.3