From d25de88dcc7e9bca96ab93bded09dfb9746018fd Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 6 Feb 2017 13:59:14 +0100 Subject: Inline fst and snd from Datatypes. This avoids nameclashes with the Pervasives version of these functions. --- extraction/extraction.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index 82b0a023..9c4c724f 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -40,6 +40,10 @@ Require Import ExtrOcamlString. (* Coqlib *) Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)". +(* Datatypes *) +Extract Inlined Constant Datatypes.fst => "fst". +Extract Inlined Constant Datatypes.snd => "snd". + (* Decidable *) Extraction Inline DecidableClass.Decidable_witness DecidableClass.decide -- cgit