Another micro-improvement in printing "fix".

Set Printing Width 20.
Check fix my_long_fix
 (my_induction_variable y z t u v w x' y' z' t' u' v' w' : nat)
 (a b c d e f a' b' c' d' e' f' : bool) :=
 match my_induction_variable with
 | 0 => 0
 | S my_recursive_variable => my_recursive_variable
 end.

gives:

fix my_long_fix
  (my_induction_variable
   y z t u v w x'
   y' z' t' u' v'
   w' : nat)
  (a b c d e f a'
   b' c' d' e'
   f' : bool)
  {struct
   my_induction_variable} :
    nat :=
  match
    my_induction_variable
  with
  | 0 => 0
  | S
    my_recursive_variable =>
      my_recursive_variable
  end

instead of:

fix
my_long_fix (my_induction_variable
            y z t u
            v w x'
            y' z'
            t' u'
            v'
            w' : nat)
            (a b c
            d e f
            a' b'
            c' d'
            e'
            f' : bool)
            {struct
            my_induction_variable} :
  nat :=
  match
    my_induction_variable
  with
  | 0 => 0
  | S
    my_recursive_variable =>
      my_recursive_variable
  end

0 files changed, 0 insertions, 0 deletions