The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Dear list

I was wondering if it was currently possible (and if not, how hard it
would be to add this possibility) to push constant out of function
definitions at extraction time, so that they are not rebuild at each
call.

For example, say I have a function like

Definition foo n :=
  if eq_nat_dec n 32 then ... else ...

The 32 is extracted as S (S (.....)) *inside* the function, triggering
32 allocations at each call of foo

I was wondering if it was possible to obtain automatically something like

Let __const51 = S (S (...))

let foo n =
  match eq_nat_dec n __const51 with
   ...

to avoid those useless allocations

Thanks

Alexandre Pilkiewicz