Squashed commit of the following:

commit 292a733fa38807c7f57da5d02d6e0af06b6ea9f4
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date:   Mon Sep 19 14:36:27 2022 +0200

    source

commit 18fe869eada19e5a2f1187b8088ec4a030747ded
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date:   Mon Sep 19 14:31:06 2022 +0200

    adjust some timings

commit 1375208fa33a6f5786e061c60517f4cafe3dcfa1
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date:   Mon Sep 19 14:28:35 2022 +0200

    attempt at correct loadimm latency

commit 59be28c0be91e9eab30c3ce2f0cc0ed6e3cfb004
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date:   Mon Sep 19 14:20:21 2022 +0200

    first attempt at Cortex-R5

This reverts commit c3d8637d.

This reverts commit 6bb2b38231ed8f18a60907df1523931a14ea350e.

- better separation middle-end/backend in LCT
- smarter pattern detection (avoid adding then removing from the
  hashmap)
- now building intermediate variables for each instruction in the
  pattern (it is needed in some specific cases)
- more precise matching: introducing a matching level for sequences

Improves robustness in case of stronger (e)auto.
This is in preparation of a change in Coq that will make auto and eauto stronger
(https://github.com/coq/coq/pull/16293).

fixing some bug about update predicate
fixing the subst-critical "pushing" function for insertion points
(there was a stack overflow sometimes)