From 93ac07bbb48ba3a2eca0d5c75aa9be7095a19912 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 2 Sep 2020 18:07:54 +0200
Subject: Document the Equality.equality type in the ML file.

---
 tactics/equality.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7ad672008e..8a406ce8c5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1015,7 +1015,9 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind =
 
 type equality = {
   eq_data  : (coq_eq_data * (EConstr.t * EConstr.t * EConstr.t));
+  (* equality data + A : Type, t1 : A, t2 : A *)
   eq_clenv : clausenv;
+  (* clause [M : R A t1 t2] where [R] is the equality from above *)
 }
 
 let eq_baseid = Id.of_string "e"
-- 
cgit v1.2.3