From e4c88054ccf30e69f58d9ead1592102ecb0a1611 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 6 Oct 2006 17:13:50 +0000
Subject: 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
---
 kernel/typeops.ml  | 2 --
 kernel/typeops.mli | 2 --
 2 files changed, 4 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3