diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-24 12:01:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-24 12:14:24 +0200 |
| commit | 1b029b2163386f20179a61f6bdb68e5532f4c306 (patch) | |
| tree | fa58a62145fa61d9823a79a04dba8571317ff4c4 | |
| parent | 3df7e2a89ae931207781c6f5cbc9e196235b1dc3 (diff) | |
Fixing a loop in checking hints with holes.
For instance, "Hint Resolve (fst _ _)." was looping (bug in 841bc461).
| -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 2755ed9cb..4ba9adafe 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 *) |