search

coq-community / reduction-effects

A Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]
Mozilla Public License 2.0
6 stars 6 forks source link

print_id in match prints nothing #10

Closed VincentSe closed 4 years ago

VincentSe commented 4 years ago

This prints nothing

From ReductionEffect Require Import PrintingEffect.
Eval cbv in (match print_id (3%nat) with
             | O => O
             | S p => 3
             end).
herbelin commented 4 years ago

A fix is available at coq/coq#12751.