diff options
| author | herbelin | 2005-05-20 15:41:56 +0000 |
|---|---|---|
| committer | herbelin | 2005-05-20 15:41:56 +0000 |
| commit | fc3eea4f6ab224df79d1c9e4350d96b639a0f923 (patch) | |
| tree | e72f41791d8eecf21992880862a64718390f8304 | |
| parent | 6b9fe746af01222454a11b4c260f09e85f132494 (diff) | |
Documentation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7047 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/detyping.mli | 6 |
1 files 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 |