Merge PR #9867: Add primitive floats (binary64 floating-point numbers)

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl

19 files changed, 163 insertions, 20 deletions

diff --git a/plugins/extraction/ExtrOCamlFloats.v b/plugins/extraction/ExtrOCamlFloats.v
new file mode 100644
index 0000000000..1891772cc2
--- /dev/null
+++ b/plugins/extraction/ExtrOCamlFloats.v
@@ -0,0 +1,61 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Extraction to OCaml of native binary64 floating-point numbers.
+
+Note: the extraction of primitive floats relies on Coq's internal file
+kernel/float64.ml, so make sure the corresponding binary is available
+when linking the extracted OCaml code.
+
+For example, if you build a (_CoqProject + coq_makefile)-based project
+and if you created an empty subfolder "extracted" and a file "test.v"
+containing [Cd "extracted". Separate Extraction function_to_extract.],
+you will just need to add in the _CoqProject: [test.v], [-I extracted]
+and the list of [extracted/*.ml] and [extracted/*.mli] files, then add
+[CAMLFLAGS += -w -33] in the Makefile.local file.  *)
+
+From Coq Require Floats Extraction.
+
+(** Basic data types used by some primitive operators. *)
+
+Extract Inductive bool => bool [ true false ].
+Extract Inductive prod => "( * )" [ "" ].
+
+Extract Inductive FloatClass.float_class =>
+  "Float64.float_class"
+  [ "PNormal" "NNormal" "PSubn" "NSubn" "PZero" "NZero" "PInf" "NInf" "NaN" ].
+Extract Inductive PrimFloat.float_comparison =>
+  "Float64.float_comparison"
+  [ "FEq" "FLt" "FGt" "FNotComparable" ].
+
+(** Primitive types and operators. *)
+
+Extract Constant PrimFloat.float => "Float64.t".
+Extraction Inline PrimFloat.float.
+(* Otherwise, the name conflicts with the primitive OCaml type [float] *)
+
+Extract Constant PrimFloat.classify => "Float64.classify".
+Extract Constant PrimFloat.abs => "Float64.abs".
+Extract Constant PrimFloat.sqrt => "Float64.sqrt".
+Extract Constant PrimFloat.opp => "Float64.opp".
+Extract Constant PrimFloat.eqb => "Float64.eq".
+Extract Constant PrimFloat.ltb => "Float64.lt".
+Extract Constant PrimFloat.leb => "Float64.le".
+Extract Constant PrimFloat.compare => "Float64.compare".
+Extract Constant PrimFloat.mul => "Float64.mul".
+Extract Constant PrimFloat.add => "Float64.add".
+Extract Constant PrimFloat.sub => "Float64.sub".
+Extract Constant PrimFloat.div => "Float64.div".
+Extract Constant PrimFloat.of_int63 => "Float64.of_int63".
+Extract Constant PrimFloat.normfr_mantissa => "Float64.normfr_mantissa".
+Extract Constant PrimFloat.frshiftexp => "Float64.frshiftexp".
+Extract Constant PrimFloat.ldshiftexp => "Float64.ldshiftexp".
+Extract Constant PrimFloat.next_up => "Float64.next_up".
+Extract Constant PrimFloat.next_down => "Float64.next_down".
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index cca212f332..04f5b66241 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -351,7 +351,7 @@ let rec extract_type env sg db j c args =
             | (Info, TypeScheme) ->
               extract_type_app env sg db (r, type_sign env sg ty) args
             | (Info, Default) -> Tunknown))
-    | Cast _ | LetIn _ | Construct _ | Int _ -> assert false
+    | Cast _ | LetIn _ | Construct _ | Int _ | Float _ -> assert false
 
 (*s Auxiliary function dealing with type application.
   Precondition: [r] is a type scheme represented by the signature [s],
@@ -690,6 +690,7 @@ let rec extract_term env sg mle mlt c args =
        let extract_var mlt = put_magic (mlt,vty) (MLglob (GlobRef.VarRef v)) in
        extract_app env sg mle mlt extract_var args
     | Int i -> assert (args = []); MLuint i
+    | Float f -> assert (args = []); MLfloat f
     | Ind _ | Prod _ | Sort _ -> assert false
 
 (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index e4efbcff0c..4769bef475 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -215,6 +215,8 @@ let rec pp_expr par env args =
     | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
     | MLuint _ ->
       pp_par par (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
+    | MLfloat _ ->
+      pp_par par (str "Prelude.error \"EXTRACTION OF FLOAT NOT IMPLEMENTED\"")
 
 and pp_cons_pat par r ppl =
   pp_par par
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index 912a20f389..81b3e1bcdc 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -161,6 +161,10 @@ let rec json_expr env = function
       ("what", json_str "expr:int");
       ("int", json_str (Uint63.to_string i))
     ]
+  | MLfloat f -> json_dict [
+      ("what", json_str "expr:float");
+      ("float", json_str (Float64.to_string f))
+    ]
 
 and json_one_pat env (ids,p,t) =
   let ids', env' = push_vars (List.rev_map id_of_mlid ids) env in json_dict [
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
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index e3c9635c55..32e0d3c05d 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -127,6 +127,7 @@ and ml_ast =
   | MLaxiom
   | MLmagic  of ml_ast
   | MLuint   of Uint63.t
+  | MLfloat  of Float64.t
 
 and ml_pattern =
   | Pcons   of GlobRef.t * ml_pattern list
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 000df26858..44b95ae4c1 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -398,6 +398,7 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with
 | MLaxiom, MLaxiom -> true
 | MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2
 | MLuint i1, MLuint i2 -> Uint63.equal i1 i2
+| MLfloat f1, MLfloat f2 -> Float64.equal f1 f2
 | _, _ -> false
 
 and eq_ml_pattern p1 p2 = match p1, p2 with
@@ -430,7 +431,7 @@ let ast_iter_rel f =
     | MLapp (a,l) -> iter n a; List.iter (iter n) l
     | MLcons (_,_,l) | MLtuple l ->  List.iter (iter n) l
     | MLmagic a -> iter n a
-    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> ()
+    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> ()
   in iter 0
 
 (*s Map over asts. *)
@@ -449,7 +450,8 @@ let ast_map f = function
   | MLcons (typ,c,l) -> MLcons (typ,c, List.map f l)
   | MLtuple l -> MLtuple (List.map f l)
   | MLmagic a -> MLmagic (f a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom
+  | MLuint _ | MLfloat _ as a -> a
 
 (*s Map over asts, with binding depth as parameter. *)
 
@@ -467,7 +469,8 @@ let ast_map_lift f n = function
   | MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l)
   | MLtuple l -> MLtuple (List.map (f n) l)
   | MLmagic a -> MLmagic (f n a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom
+  | MLuint _ | MLfloat _ as a -> a
 
 (*s Iter over asts. *)
 
@@ -481,7 +484,8 @@ let ast_iter f = function
   | MLapp (a,l) -> f a; List.iter f l
   | MLcons (_,_,l) | MLtuple l -> List.iter f l
   | MLmagic a -> f a
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> ()
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom
+  | MLuint _ | MLfloat _ -> ()
 
 (*S Operations concerning De Bruijn indices. *)
 
@@ -517,7 +521,7 @@ let nb_occur_match =
     | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
     | MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l
     | MLmagic a -> nb k a
-    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> 0
+    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> 0
   in nb 1
 
 (* Replace unused variables by _ *)
@@ -569,7 +573,7 @@ let dump_unused_vars a =
        let b' = ren env b in
        if b' == b then a else MLmagic b'
 
-    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> a
+    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ | MLfloat _ -> a
 
     and ren_branch env ((ids,p,b) as tr) =
       let occs = List.map (fun _ -> ref false) ids in
@@ -1402,7 +1406,8 @@ let rec ml_size = function
   | MLfix(_,_,f) -> ml_size_array f
   | MLletin (_,_,t) -> ml_size t
   | MLmagic t -> ml_size t
-  | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom | MLuint _ -> 0
+  | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom
+  | MLuint _ | MLfloat _ -> 0
 
 and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l
 
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 6b1eef7abb..fe49bfc1ec 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -107,7 +107,7 @@ let ast_iter_references do_term do_cons do_type a =
 	Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v
 
       | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _
-      | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ -> ()
+      | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ | MLfloat _ -> ()
   in iter a
 
 let ind_iter_references do_term do_cons do_type kn ind =
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index e7004fe9af..34ddf57b40 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -307,6 +307,9 @@ let rec pp_expr par env args =
     | MLuint i ->
         assert (args=[]);
         str "(" ++ str (Uint63.compile i) ++ str ")"
+    | MLfloat f ->
+        assert (args=[]);
+        str "(" ++ str (Float64.compile f) ++ str ")"
 
 
 and pp_record_proj par env typ t pv args =
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index dd840cd929..c341ec8d57 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -131,6 +131,8 @@ let rec pp_expr env args =
     | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
     | MLuint _ ->
       paren (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
+    | MLfloat _ ->
+      paren (str "Prelude.error \"EXTRACTION OF FLOAT NOT IMPLEMENTED\"")
 
 and pp_cons_args env = function
   | MLcons (_,r,args) when is_coinductive r ->
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 7be049269c..6db0a1119b 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -692,13 +692,14 @@ let build_proof
               end
           | Cast(t,_,_) ->
               build_proof do_finalize {dyn_infos with info = t} g
-          | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
+          | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ | Float _ ->
               do_finalize dyn_infos g
           | App(_,_) ->
               let f,args = decompose_app sigma dyn_infos.info in
               begin
                 match EConstr.kind sigma f with
-      | Int _ -> user_err Pp.(str "integer cannot be applied")
+                  | Int _ -> user_err Pp.(str "integer cannot be applied")
+                  | Float _ -> user_err Pp.(str "float cannot be applied")
                   | App _ -> assert false (* we have collected all the app in decompose_app *)
                   | Proj _ -> assert false (*FIXME*)
                   | Var _ | Construct _ | Rel _ | Evar _ | Meta _  | Ind _ | Sort _ | Prod _ ->
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 0452665585..6add56dd5b 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -68,7 +68,7 @@ let is_rec names =
   let check_id id names =  Id.Set.mem id names in
   let rec lookup names gt = match DAst.get gt with
     | GVar(id) -> check_id id names
-    | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ | GInt _ -> false
+    | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ | GInt _ | GFloat _ -> false
     | GCast(b,_) -> lookup names b
     | GRec _ -> CErrors.user_err (Pp.str "GRec not handled")
     | GIf(b,_,lhs,rhs) ->
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 7c17ecdba0..895b6a37ee 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -478,7 +478,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
   observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt);
   let open CAst in
   match DAst.get rt with
-    | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _  | GHole _ | GInt _ ->
+    | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _  | GHole _ | GInt _ | GFloat _ ->
 	(* do nothing (except changing type of course) *)
 	mk_result [] rt avoid
     | GApp(_,_) ->
@@ -590,6 +590,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret
 	    | GRec _ -> user_err Pp.(str "Not handled GRec")
 	    | GProd _ -> user_err Pp.(str "Cannot apply a type")
             | GInt _ -> user_err Pp.(str "Cannot apply an integer")
+      | GFloat _ -> user_err Pp.(str "Cannot apply a float")
 	end (* end of the application treatement *)
 
     | GLambda(n,_,t,b) ->
@@ -1231,7 +1232,7 @@ let rebuild_cons env nb_args relname args crossed_types rt =
    TODO: Find a valid way to deal with implicit arguments here!
 *)
 let rec compute_cst_params relnames params gt = DAst.with_val (function
-  | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ -> params
+  | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ | GFloat _ -> params
   | GApp(f,args) ->
     begin match DAst.get f with
     | GVar relname' when Id.Set.mem relname' relnames ->
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 8abccabae6..5f54bad598 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -115,6 +115,7 @@ let change_vars =
       | GSort _ as x -> x
       | GHole _ as x -> x
       | GInt _ as x -> x
+      | GFloat _ as x -> x
       | GCast(b,c) ->
 	  GCast(change_vars mapping b,
                 Glob_ops.map_cast_type (change_vars mapping) c)
@@ -295,6 +296,7 @@ let rec alpha_rt excluded rt =
     | GRec _ -> user_err Pp.(str "Not handled GRec")
     | GSort _
     | GInt _
+    | GFloat _
     | GHole _ as rt -> rt
     | GCast (b,c) ->
 	GCast(alpha_rt excluded b,
@@ -354,7 +356,7 @@ let is_free_in id =
     | GHole _ -> false
     | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
     | GCast (b,CastCoerce) -> is_free_in b
-    | GInt _ -> false
+    | GInt _ | GFloat _ -> false
     ) x
   and is_free_in_br {CAst.v=(ids,_,rt)} =
     (not (Id.List.mem id ids)) && is_free_in rt
@@ -447,6 +449,7 @@ let replace_var_by_term x_id term =
       | GSort _
       | GHole _ as rt -> rt
       | GInt _ as rt -> rt
+      | GFloat _ as rt -> rt
       | GCast(b,c) ->
 	  GCast(replace_var_by_pattern b,
                 Glob_ops.map_cast_type replace_var_by_pattern c)
@@ -529,7 +532,7 @@ let expand_as =
       | PatCstr(_,patl,_) -> List.fold_left add_as map patl
   in
   let rec expand_as map = DAst.map (function
-      | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ as rt -> rt
+      | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ | GFloat _ as rt -> rt
       | GVar id as rt ->
 	  begin
 	    try
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 29356df81d..66ed1961ba 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -270,7 +270,7 @@ let check_not_nested env sigma forbidden e =
   let rec check_not_nested e =
     match EConstr.kind sigma e with
       | Rel _ -> ()
-      | Int _ -> ()
+      | Int _ | Float _ -> ()
       | Var x ->
         if Id.List.mem x forbidden
         then user_err ~hdr:"Recdef.check_not_nested"
@@ -452,7 +452,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
           | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env env sigma expr_info.info ++ Pp.str ".")
       end
     | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g
-    | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ ->
+    | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ | Float _ ->
       let new_continuation_tac =
         jinfo.otherS () expr_info continuation_tac in
       new_continuation_tac expr_info g
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 4d7a04f5ee..9682487a22 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -319,7 +319,7 @@ let iter_constr_LR f c = match kind c with
     for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done
   | Proj(_,a) -> f a
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _ | Construct _
-     | Int _) -> ()
+     | Int _ | Float _) -> ()
 
 (* The comparison used to determine which subterms matches is KEYED        *)
 (* CONVERSION. This looks for convertible terms that either have the same  *)
diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml
new file mode 100644
index 0000000000..3c2e217d1c
--- /dev/null
+++ b/plugins/syntax/float_syntax.ml
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Glob_term
+
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "float_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
+(*** Constants for locating float constructors ***)
+
+let make_dir l = DirPath.make (List.rev_map Id.of_string l)
+let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
+
+(*** Parsing for float in digital notation ***)
+
+let interp_float ?loc (sign,n) =
+  let sign = Constrexpr.(match sign with SPlus -> "" | SMinus -> "-") in
+  DAst.make ?loc (GFloat (Float64.of_string (sign ^ NumTok.to_string n)))
+
+(* Pretty printing is already handled in constrextern.ml *)
+
+let uninterp_float _ = None
+
+(* Actually declares the interpreter for float *)
+
+open Notation
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
+let float_module = ["Coq"; "Floats"; "PrimFloat"]
+let float_path = make_path float_module "float"
+let float_scope = "float_scope"
+
+let _ =
+  register_rawnumeral_interpretation float_scope (interp_float,uninterp_float);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_local = false;
+      pt_scope = float_scope;
+      pt_interp_info = Uid float_scope;
+      pt_required = (float_path,float_module);
+      pt_refs = [];
+      pt_in_match = false }
diff --git a/plugins/syntax/float_syntax_plugin.mlpack b/plugins/syntax/float_syntax_plugin.mlpack
new file mode 100644
index 0000000000..d69f49bcfe
--- /dev/null
+++ b/plugins/syntax/float_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Float_syntax
diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune
index 7a23581768..512752135d 100644
--- a/plugins/syntax/plugin_base.dune
+++ b/plugins/syntax/plugin_base.dune
@@ -25,3 +25,10 @@
  (synopsis "Coq syntax plugin: int63")
  (modules int63_syntax)
  (libraries coq.vernac))
+
+(library
+ (name float_syntax_plugin)
+ (public_name coq.plugins.float_syntax)
+ (synopsis "Coq syntax plugin: float")
+ (modules float_syntax)
+ (libraries coq.vernac))