diff options
Diffstat (limited to 'pretyping/glob_ops.ml')
| -rw-r--r-- | pretyping/glob_ops.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 93f5923474..03bb633fa0 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -156,9 +156,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with | GCast (c1, t1), GCast (c2, t2) -> f c1 c2 && cast_type_eq f t1 t2 | GInt i1, GInt i2 -> Uint63.equal i1 i2 + | GFloat f1, GFloat f2 -> Float64.equal f1 f2 | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ | - GInt _), _ -> false + GInt _ | GFloat _), _ -> false let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c @@ -219,7 +220,7 @@ let map_glob_constr_left_to_right f = DAst.map (function let comp1 = f c in let comp2 = map_cast_type f k in GCast (comp1,comp2) - | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _) as x -> x + | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) as x -> x ) let map_glob_constr = map_glob_constr_left_to_right @@ -251,7 +252,7 @@ let fold_glob_constr f acc = DAst.with_val (function let acc = match k with | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in f acc c - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _) -> acc + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc ) let fold_return_type_with_binders f g v acc (na,tyopt) = Option.fold_left (f (Name.fold_right g na v)) acc tyopt @@ -293,7 +294,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function let acc = match k with | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in f v acc c - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _) -> acc)) + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GInt _ | GFloat _) -> acc)) let iter_glob_constr f = fold_glob_constr (fun () -> f) () |