diff options
Diffstat (limited to 'plugins/funind/glob_termops.mli')
| -rw-r--r-- | plugins/funind/glob_termops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 70211a1860..bdde66bbd7 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -101,8 +101,8 @@ val ids_of_pat : cases_pattern -> Id.Set.t val expand_as : glob_constr -> glob_constr -(* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution +(* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution *) val resolve_and_replace_implicits : - ?flags:Pretyping.inference_flags -> + ?flags:Pretyping.inference_flags -> ?expected_type:Pretyping.typing_constraint -> Environ.env -> Evd.evar_map -> glob_constr -> glob_constr |