From b97c6e7e86bce3a6ec7a9e3b99cfc08067f00789 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 1 Dec 1999 10:52:21 +0000
Subject: diverses fonctions ajoutees

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@170 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/term.ml')

diff --git a/kernel/term.ml b/kernel/term.ml
index 91061c7ca3..1a5c74e682 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -69,6 +69,7 @@ let make_typed t s = { body = t; typ = s }
 let typed_app f tt = { body = f tt.body; typ = tt.typ }
 
 let body_of_type ty = ty.body
+let level_of_type t = (t.typ : sorts)
 
 let incast_type tty = DOP2 (Cast, tty.body, (DOP0 (Sort tty.typ)))
 
-- 
cgit v1.2.3