diff options
Diffstat (limited to 'pretyping/clenv.mli')
| -rw-r--r-- | pretyping/clenv.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 73a171b8d..8546a44ef 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -61,7 +61,8 @@ val mk_clenv_type_of : evar_info sigma -> constr -> clausenv (* linking of clenvs *) val connect_clenv : evar_info sigma -> clausenv -> clausenv -val clenv_fchain : metavariable -> clausenv -> clausenv -> clausenv +val clenv_fchain : + ?allow_K:bool -> metavariable -> clausenv -> clausenv -> clausenv (***************************************************************) (* Unification with clenvs *) |