diff options
| author | Pierre-Marie Pédrot | 2015-10-26 15:55:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-26 15:55:15 +0100 |
| commit | aff038fbbe5ade8d58a895b3d2f6e32267c5184c (patch) | |
| tree | 0598bda5a6432894e4fec9ac071cf9ad544d3ee2 /tactics/hints.ml | |
| parent | 010775eba60ea89645792b48a0686ff15c4ebcb5 (diff) | |
| parent | 6417a9e72feb39b87f0b456186100b11d1c87d5f (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 2755ed9cb0..4ba9adafec 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1071,7 +1071,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = (* We skip the test whether args is the identity or not *) let t = Evarutil.nf_evar sigma (existential_type sigma ev) in let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in - if not (Int.Set.is_empty (free_rels t)) then + if not (closed0 c) then error "Hints with holes dependent on a bound variable not supported."; if occur_existential t then (* Not clever enough to construct dependency graph of evars *) |