From d306f5428db0d034aea55d3f0699c67c1f296cc1 Mon Sep 17 00:00:00 2001
From: JPR
Date: Thu, 23 May 2019 23:28:55 +0200
Subject: Fixing typos - Part 3

---
 plugins/ssr/ssrequality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 59fc69f100..538d0c4e9a 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -313,7 +313,7 @@ let rw_progress rhs lhs ise = not (EConstr.eq_constr ise lhs (Evarutil.nf_evar i
 (* Coq has a more general form of "equation" (any type with a single *)
 (* constructor with no arguments with_rect_r elimination lemmas).    *)
 (* However there is no clear way of determining the LHS and RHS of   *)
-(* such a generic Leibniz equation -- short of inspecting the type  *)
+(* such a generic Leibniz equation -- short of inspecting the type   *)
 (* of the elimination lemmas.                                        *)
 
 let rec strip_prod_assum c = match Constr.kind c with
-- 
cgit v1.2.3