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

4 files changed, 12 insertions, 4 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 4b5a6e01a8..0d2874cb76 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -49,8 +49,6 @@ let assumption_of_judgment env j =
 
 let sort_judgment env j = (type_judgment env j).utj_type
 
-let on_judgment_type f j = { j with uj_type = f j.uj_type }
-
 (************************************************)
 (* Incremental typing rules: builds a typing judgement given the *)
 (* judgements for the subterms. *)
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 6e20cd42d7..516caf3ed5 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -33,8 +33,6 @@ val infer_local_decls :
 
 val assumption_of_judgment :  env -> unsafe_judgment -> types
 val type_judgment          :  env -> unsafe_judgment -> unsafe_type_judgment
-val on_judgment_type       :  
-  (types -> types) -> unsafe_judgment -> unsafe_judgment
 
 (*s Type of sorts. *)
 val judge_of_prop_contents : contents -> unsafe_judgment
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