diff options
Diffstat (limited to 'kernel/nativelambda.ml')
| -rw-r--r-- | kernel/nativelambda.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 70b3beb2dc..301773143c 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -580,6 +580,8 @@ let rec lambda_of_constr cache env sigma c = | Int i -> Luint i + | Float _ -> assert false (* native computed for primitive float not yet implemented *) + and lambda_of_app cache env sigma f args = match kind f with | Const (_kn,_u as c) -> |