From b0004f8f03eb7d1a050129115cfd79b11873b631 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 19 Sep 2001 16:56:26 +0000
Subject: Nouvelle fonction get_sort_family_of pour calculer la famille dans
 lequel vit un type

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2010 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/retyping.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 2e32601d9f..c8ef3d2e5b 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -24,8 +24,10 @@ open Environ
 type metamap = (int * constr) list
 
 val get_type_of : env -> 'a evar_map -> constr -> constr
+val get_sort_of : env -> 'a evar_map -> types -> sorts
+val get_sort_family_of : env -> 'a evar_map -> types -> sorts_family
+
 val get_type_of_with_meta : env -> 'a evar_map -> metamap -> constr -> constr
-val get_sort_of : env -> 'a evar_map -> constr -> sorts
 
 (* Makes an assumption from a constr *)
 val get_assumption_of : env -> 'a evar_map -> constr -> types
-- 
cgit v1.2.3