diff options
| author | Pierre-Marie Pédrot | 2020-09-02 18:07:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-02 18:08:58 +0200 |
| commit | 93ac07bbb48ba3a2eca0d5c75aa9be7095a19912 (patch) | |
| tree | b21c5acb87a9330243f73a52bcca1ad72a9bdd72 | |
| parent | 8f484215c8f9beddeffbf0787dbd23265dddfc29 (diff) | |
Document the Equality.equality type in the ML file.
| -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" |