aboutsummaryrefslogtreecommitdiff
path: root/vernac/recLemmas.ml
AgeCommit message (Expand)Author
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
2020-06-26[recLemmas] Nit on naming consistency.Emilio Jesus Gallego Arias
2020-06-26[declare] Improve organization of proof/constant information.Emilio Jesus Gallego Arias
2020-06-26[declare] Use Recthm.t in mutual analysis functionsEmilio Jesus Gallego Arias
2020-06-26[declare] Refactor analysis and construction of mutual lemmasEmilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-07-07[lemmas] Move mutually recursive lemma analysis to its own module.Emilio Jesus Gallego Arias