diff options
Diffstat (limited to 'plugins/ring/ring.ml')
| -rw-r--r-- | plugins/ring/ring.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 6ee12ebcb..c0b5542ee 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -258,7 +258,7 @@ let subst_theory subst th = } -let subst_th (_,subst,(c,th as obj)) = +let subst_th (subst,(c,th as obj)) = let c' = subst_mps subst c in let th' = subst_theory subst th in if c' == c && th' == th then obj else |