diff options
| -rw-r--r-- | tactics/equality.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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" |