diff options
Diffstat (limited to 'contrib/romega/ReflOmegaCore.v')
| -rw-r--r-- | contrib/romega/ReflOmegaCore.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v index 903fc63d07..fa49badbf3 100644 --- a/contrib/romega/ReflOmegaCore.v +++ b/contrib/romega/ReflOmegaCore.v @@ -701,7 +701,7 @@ Definition Tplus_assoc_l [t: term] := Theorem Tplus_assoc_l_stable : (term_stable Tplus_assoc_l). -(ProveStable Tplus_assoc_l Zplus_assoc_l). +(ProveStable Tplus_assoc_l Zplus_assoc). Save. Definition Tplus_assoc_r [t: term] := |