diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 25 |
1 files changed, 5 insertions, 20 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index efe1525c9a..13bd8f7718 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -816,26 +816,11 @@ let map_constr_with_full_binders_user_view sigma g f = each binder traversal; it is not recursive *) let fold_constr_with_full_binders sigma g f n acc c = - let open RelDecl in - match EConstr.kind sigma c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> acc - | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c - | Lambda (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g (LocalDef (na, b, t)) n) (f n (f n acc b) t) c - | App (c,l) -> Array.fold_left (f n) (f n acc c) l - | Proj (p,c) -> f n acc c - | Evar (_,l) -> Array.fold_left (f n) acc l - | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl - | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + let open EConstr in + let f l acc c = f l acc (of_constr c) in + let g d l = g (of_rel_decl d) l in + let c = Unsafe.to_constr (whd_evar sigma c) in + Constr.fold_with_full_binders g f n acc c let fold_constr_with_binders sigma g f n acc c = fold_constr_with_full_binders sigma (fun _ x -> g x) f n acc c |