diff options
| author | Pierre Roux | 2018-08-28 18:56:07 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:35 +0100 |
| commit | d18b928154a48ff8d90aaff69eca7d6eb3dfa0ab (patch) | |
| tree | 9cc9b39b16849ed839f4adf7b19e3d3291f7dd98 /vernac | |
| parent | 79605dabb10e889ae998bf72c8483f095277e693 (diff) | |
Implement classify on primitive float
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_vernac.mlg | 1 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 78e4c89521..aeae86e1f7 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -276,6 +276,7 @@ GRAMMAR EXTEND Gram | "#float64_opp" -> { CPrimitives.Float64opp } | "#float64_abs" -> { CPrimitives.Float64abs } | "#float64_compare" -> { CPrimitives.Float64compare } + | "#float64_classify" -> { CPrimitives.Float64classify } | "#float64_add" -> { CPrimitives.Float64add } | "#float64_sub" -> { CPrimitives.Float64sub } | "#float64_mul" -> { CPrimitives.Float64mul } diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index c86b70c78e..c4892736ae 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1848,6 +1848,7 @@ let vernac_register qid r = | "ind_pair" -> CPrimitives.(PIE PIT_pair) | "ind_cmp" -> CPrimitives.(PIE PIT_cmp) | "ind_f_cmp" -> CPrimitives.(PIE PIT_f_cmp) + | "ind_f_class" -> CPrimitives.(PIE PIT_f_class) | k -> CErrors.user_err Pp.(str "Register: unknown identifier “" ++ str k ++ str "” in the “kernel” namespace") in match gr with |