aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/clenv.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/clenv.mli')
-rw-r--r--pretyping/clenv.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 090b9c661..9ad64e31d 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -108,6 +108,8 @@ val make_clenv_binding :
(* other stuff *)
val clenv_environments :
evar_defs -> int option -> types -> evar_defs * constr list * types
+val clenv_environments_evars :
+ env -> evar_defs -> int option -> types -> evar_defs * constr list * types
(***************************************************************)
(* Pretty-print *)