| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-07-31 | Fix #7348: extraction of dependent record projections | Kazuhiko Sakaguchi | |
| - Inline record projections by default (except for Haskell extraction). - Extend `pp_record_proj` for record projections involving `MLmagic`. - Remove special treatments for pretty-printing for record projections other than `pp_record_proj`. - `micromega.ml` had to be changed due to this change of the extraction plugin. Acknowledgement: This work is financially supported by Peano System Inc. on-behalf-of: @peano-system <info@peano-system.jp> | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |