| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-08-10 | [extraction] Fix #7191: Avoid unsound eta-reduction | Kazuhiko Sakaguchi | |
| `Mlutil.simpl` and `Mlutil.atomic_eta_red` did some unsound eta-reductions as follows: (fun x0 ... xn => MLexn x0 ... xn) ->eta MLexn. `MLexn` raises an exception thus is not a value in OCaml. So the above simplification may change the behavior of extracted programs. This patch restricts `atomic_eta_red` to eta-redexes whose core is both atomic and value. 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 |