diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-09 15:19:08 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-10-09 15:21:17 +0200 |
| commit | f3c4dc6fb350b318ccc3af3a0e9aecb977b25744 (patch) | |
| tree | 3ed3921b242f0129e33d76b59939b44249041e1b /tactics/hints.mli | |
| parent | d694c532f3f15569a204fa9f2d02f2c0ea83b424 (diff) | |
Fix CFGV contrib: handling of global hints introducing global universes.
It was wrong, the context was readded needlessly to the local evar_map context.
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 5a4fb7709..b7b219e2e 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -151,8 +151,8 @@ val interp_hints : polymorphic -> hints_expr -> hints_entry val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit -val prepare_hint : bool (* Check no remaining evars *) -> env -> evar_map -> - open_constr -> hint_term +val prepare_hint : bool (* Check no remaining evars *) -> bool (* polymorphic *) -> + env -> evar_map -> open_constr -> hint_term (** [make_exact_entry pri (c, ctyp)]. [c] is the term given as an exact proof to solve the goal; |