diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/clenv.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index b855ee7e0a..944d7d4b39 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -81,6 +81,8 @@ val clenv_unique_resolver : val evar_clenv_unique_resolver : clausenv -> evar_info sigma -> clausenv +val clenv_pose_dependent_evars : clausenv -> clausenv + (***************************************************************) (* Bindings *) |