Small improvement to "fix"/"cofix" printing rule.

Set Implicit Arguments.
Set Contextual Implicit.
Inductive option A := None | Some (a:A).
Coercion some_nat := @Some nat.
Check fix f x := match x with 0 => None | n => some_nat n end.

gives:

fix f (x : nat) : option nat :=
  match x with
  | 0 => None (A:=nat)
  | S _ => some_nat x
  end

See discussion at
https://github.com/coq/coq/pull/11142/files/718c1422954794e0e33a87cf4c9111c00cc186dd#r377054717

0 files changed, 0 insertions, 0 deletions