diff options
| author | Maxime Dénès | 2019-11-01 15:53:30 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-11-01 15:53:30 +0100 |
| commit | fdabd4dbd6bfd60ad46fc8c945ed063860498e53 (patch) | |
| tree | 01edf91f8b536ad4acfbba39e114daa06b40f3f8 /pretyping/typing.ml | |
| parent | d00c0b93ec4cb5ca48a9dc2ddf2cfd2038208ee2 (diff) | |
| parent | acdaab2a8c2ccb63df364bb75de8a515b2cef484 (diff) | |
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
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 2db5512ff4..1a145fe1b2 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -319,6 +319,9 @@ let type_of_constructor env sigma ((ind,_ as ctor),u) = let judge_of_int env v = Environ.on_judgment EConstr.of_constr (judge_of_int env v) +let judge_of_float env v = + Environ.on_judgment EConstr.of_constr (judge_of_float env v) + (* cstr must be in n.f. w.r.t. evars and execute returns a judgement where both the term and type are in n.f. *) let rec execute env sigma cstr = @@ -430,6 +433,9 @@ let rec execute env sigma cstr = | Int i -> sigma, judge_of_int env i + | Float f -> + sigma, judge_of_float env f + and execute_recdef env sigma (names,lar,vdef) = let sigma, larj = execute_array env sigma lar in let sigma, lara = Array.fold_left_map (assumption_of_judgment env) sigma larj in |