From fc3eea4f6ab224df79d1c9e4350d96b639a0f923 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 20 May 2005 15:41:56 +0000
Subject: Documentation

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

diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index e4aa8a6573..9f315938c8 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -21,8 +21,10 @@ open Mod_subst
 
 val subst_raw : substitution -> rawconstr -> rawconstr
 
-(* [detype env avoid nenv c] turns [c], typed in [env], into a rawconstr. *)
-(* De Bruijn indexes are turned to bound names, avoiding names in [avoid] *)
+(* [detype (b,env) avoid ctx c] turns [c], typed in [env], into a rawconstr *)
+(* de Bruijn indexes are turned to bound names, avoiding names in [avoid] *)
+(* [b] tells if naming must avoid global-level synonyms as intro does *)
+(* [ctx] gives the names of the free variables *)
 
 val detype : bool * env -> identifier list -> names_context -> constr -> 
   rawconstr
-- 
cgit v1.2.3