diff options
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/ring.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 2418e1abe9..9085041d37 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -535,7 +535,6 @@ let polynom_unfold_tac = { r_beta = true; r_delta = (function | Const sp -> SectionPathSet.mem sp constants_to_unfold - | Abst sp -> SectionPathSet.mem sp constants_to_unfold | _ -> false); r_iota = true }) in |