diff options
| author | Pierre-Marie Pédrot | 2020-06-08 16:21:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-19 16:02:25 +0200 |
| commit | 437f86aaa55bbae99742b600bb52a234d75667e5 (patch) | |
| tree | 296e33f16d93aab1fc733f66cee888d2248b2105 /tactics/class_tactics.ml | |
| parent | 21b4e41544f03de18d9f5b1bdb93a26b36a97999 (diff) | |
Remove access to hint section variables.
The only use was seemingly a bug introduced in 0aec9033a by an accidental
variable capture. There is indeed no reason that the set of variables of a
hint corresponds to the one of the current environment.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 2c9d06f5b9..b435d560c7 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -350,7 +350,6 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm let b = FullHint.priority h in let poly = FullHint.is_polymorphic h in let p = FullHint.pattern h in - let secvars = FullHint.secvars h in (* The use below looks suspicious *) let name = FullHint.name h in let tac = function | Res_pf (term,cl) -> |