From 3afaf3dde673d77cacaabc354f008dfbe49a7cee Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 24 Jul 2000 13:39:23 +0000
Subject: Passage à des contextes de vars et de rels pouvant contenir des
 déclarations

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

(limited to 'pretyping/detyping.mli')

diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 9e0a30d09e..e961cfe917 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -5,6 +5,7 @@
 open Names
 open Term
 open Sign
+open Environ
 open Rawterm
 (*i*)
 
@@ -13,11 +14,10 @@ open Rawterm
 
 exception StillDLAM
 
-val detype : identifier list -> unit assumptions -> constr -> rawconstr
+val detype : identifier list -> names_context -> constr -> rawconstr
 
 (* look for the index of a named var or a nondep var as it is renamed *)
-val lookup_name_as_renamed :
-  unit assumptions -> constr -> identifier -> int option
+val lookup_name_as_renamed : var_context -> constr -> identifier -> int option
 val lookup_index_as_renamed : constr -> int -> int option
 
 
-- 
cgit v1.2.3