From 3cb32772ccd0f2882a40d7f75b044b738adadad3 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 22 Oct 2019 11:57:16 +0200 Subject: Add extraction for primitive floats Co-authored-by: Pierre Roux --- plugins/extraction/miniml.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'plugins/extraction/miniml.ml') diff --git a/plugins/extraction/miniml.ml b/plugins/extraction/miniml.ml index 8b69edbe4c..32e0d3c05d 100644 --- a/plugins/extraction/miniml.ml +++ b/plugins/extraction/miniml.ml @@ -126,7 +126,8 @@ and ml_ast = | MLdummy of kill_reason | MLaxiom | MLmagic of ml_ast - | MLuint of Uint63.t + | MLuint of Uint63.t + | MLfloat of Float64.t and ml_pattern = | Pcons of GlobRef.t * ml_pattern list -- cgit v1.2.3