diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/termops.ml | 6 | ||||
| -rw-r--r-- | pretyping/termops.mli | 6 |
2 files changed, 12 insertions, 0 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index af90b91d32..252961834f 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -1020,3 +1020,9 @@ let rec rename_bound_var env l c = | Cast (c,k,t) -> mkCast (rename_bound_var env l c, k,t) | x -> c +(* Combinators on judgments *) + +let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type } +let on_judgment_value f j = { j with uj_val = f j.uj_val } +let on_judgment_type f j = { j with uj_type = f j.uj_type } + diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 5bd79a8ee1..c635dc887a 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -203,3 +203,9 @@ val global_vars_set_of_decl : env -> named_declaration -> Idset.t (* Test if an identifier is the basename of a global reference *) val is_section_variable : identifier -> bool + +(* Combinators on judgments *) + +val on_judgment : (types -> types) -> unsafe_judgment -> unsafe_judgment +val on_judgment_value : (types -> types) -> unsafe_judgment -> unsafe_judgment +val on_judgment_type : (types -> types) -> unsafe_judgment -> unsafe_judgment |