diff options
| author | herbelin | 2006-10-06 17:13:50 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-06 17:13:50 +0000 |
| commit | e4c88054ccf30e69f58d9ead1592102ecb0a1611 (patch) | |
| tree | 2f4faa03b61d33a7bfc626576c9a484a027f7198 /pretyping | |
| parent | 96ddae4e7edc653375bebf622251cde636fb1c32 (diff) | |
Déplacement de on_judgment_type de Typeops vers Termops
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9221 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |