diff options
Diffstat (limited to 'kernel/context.ml')
| -rw-r--r-- | kernel/context.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/kernel/context.ml b/kernel/context.ml index 3d98381fbb..1cc6e79485 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -134,6 +134,15 @@ struct let ty' = f ty in if v == v' && ty == ty' then decl else LocalDef (na, v', ty') + let map_constr_het f = function + | LocalAssum (na, ty) -> + let ty' = f ty in + LocalAssum (na, ty') + | LocalDef (na, v, ty) -> + let v' = f v in + let ty' = f ty in + LocalDef (na, v', ty') + (** Perform a given action on all terms in a given declaration. *) let iter_constr f = function | LocalAssum (_,ty) -> f ty |