diff options
| author | Maxime Dénès | 2017-06-04 08:06:10 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-04 08:06:10 +0200 |
| commit | b91f5d1adbd039809e31b5311d06b376829de1fc (patch) | |
| tree | c544fdd0ecb68f048077441d0faa47e36af4a4a3 /plugins/funind/glob_termops.mli | |
| parent | a2a98a4015311af83edcf8fc87aa30a5318bead8 (diff) | |
| parent | c643a4c20b033c27b153d186128093791b687b77 (diff) | |
Merge PR#526: solving implicit resolution in Function
Diffstat (limited to 'plugins/funind/glob_termops.mli')
| -rw-r--r-- | plugins/funind/glob_termops.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 25d79582f3..99a258de98 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -119,3 +119,10 @@ val zeta_normalize : Glob_term.glob_constr -> Glob_term.glob_constr 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 + *) +val resolve_and_replace_implicits : + ?flags:Pretyping.inference_flags -> + ?expected_type:Pretyping.typing_constraint -> Environ.env -> Evd.evar_map -> glob_constr -> glob_constr |