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 --
 1 file changed, 2 deletions(-)

(limited to 'kernel/typeops.ml')

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