aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/equality.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ea7967bb1d..f51751359e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -201,7 +201,7 @@ let abstract_replace clause c2 c1 unsafe tac gl =
]
] gl
else
- error "terms does not have convertible types"
+ error "terms do not have convertible types"
let replace c2 c1 gl = abstract_replace None c2 c1 false tclIDTAC gl