diff options
Diffstat (limited to 'pretyping/clenv.mli')
| -rw-r--r-- | pretyping/clenv.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 2e8057cb04..090b9c6610 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -105,6 +105,10 @@ val make_clenv_binding_apply : val make_clenv_binding : evar_info sigma -> constr * constr -> constr Rawterm.bindings -> clausenv +(* other stuff *) +val clenv_environments : + evar_defs -> int option -> types -> evar_defs * constr list * types + (***************************************************************) (* Pretty-print *) val pr_clenv : clausenv -> Pp.std_ppcmds |