diff options
Diffstat (limited to 'pretyping/detyping.mli')
| -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 |