diff options
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 823da969..9b8764f2 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: termops.ml 8845 2006-05-23 07:41:58Z herbelin $ *) +(* $Id: termops.ml 9314 2006-10-29 20:11:08Z herbelin $ *) open Pp open Util @@ -855,7 +855,12 @@ let next_global_ident_away allow_secvar id avoid = else next_global_ident_from allow_secvar (lift_ident id) avoid -(* Nouvelle version de renommage des variables (DEC 98) *) +let isGlobalRef c = + match kind_of_term c with + | Const _ | Ind _ | Construct _ | Var _ -> true + | _ -> false + +(* nouvelle version de renommage des variables (DEC 98) *) (* This is the algorithm to display distinct bound variables - Règle 1 : un nom non anonyme, même non affiché, contribue à la liste @@ -1020,3 +1025,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 } + |