From e73d5db97cdb22cce2ee479469f62af3c4b6264a Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 8 Jul 2016 14:43:57 +0200
Subject: Port to Coq 8.5pl2

Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
---
 extraction/extraction.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'extraction')

diff --git a/extraction/extraction.v b/extraction/extraction.v
index 6788bd60..e7f2e2fc 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -166,4 +166,6 @@ Separate Extraction
    Machregs.mregs_for_operation Machregs.mregs_for_builtin
    Machregs.two_address_op Machregs.is_stack_reg
    AST.signature_main
+   Floats.Float32.from_parsed Floats.Float.from_parsed
+   Globalenvs.Senv.invert_symbol
    Parser.translation_unit_file.
-- 
cgit