diff options
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 23d066df58..46a80239cf 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -76,6 +76,7 @@ let mkProj (p, c) = of_kind (Proj (p, c)) let mkArrow t1 r t2 = of_kind (Prod (make_annot Anonymous r, t1, t2)) let mkArrowR t1 t2 = mkArrow t1 Sorts.Relevant t2 let mkInt i = of_kind (Int i) +let mkFloat f = of_kind (Float f) let mkRef (gr,u) = let open GlobRef in match gr with | ConstRef c -> mkConstU (c,u) @@ -334,7 +335,7 @@ let iter_with_full_binders sigma g f n c = let open Context.Rel.Declaration in match kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> () + | Construct _ | Int _ | Float _) -> () | Cast (c,_,t) -> f n c; f n t | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c |