Remove accumulator-based functions from the semantics

[charguer]

Ideally, auxiliary functions used in the semantics should have the simplest possible presentation, and not use accumulators.

E.g. pat_bindings currently has type pat -> list varN -> list varN but it should be pat > list varN. There might be a few other occurrences.

[charguer]

Fixpoint pat_bindings (p : pat) : list varN :=
  match p with
  | Pany => []
  | Pvar n => n :: []
  | Plit l => []
  | Pcon _ ps => List.fold_right (fun p acc => acc ++ pat_bindings p) [] ps
  | Pref p => pat_bindings p
  | Ptannot p _ => pat_bindings p
  end.

[charguer]

Another occurence is pmatch, which takes as last argument an env. I think this accumulator could be avoided, simply by making pmatch_list concatenate the list of bindings that it gathers, rather than extending the accumulator as it recurses.