Extraction: more factorization of common match branches

In addition to the "| _ -> cst" situation, now we can also
 reconstruct a "| e -> f e" final branch. For instance,
 this has a tremenduous effect on Compcert/backend/Selection.v.

 NB: The "fun" factorisation is almost more general than the "cst"
 situation, but not always. Think of A=>A|B=>A, 1st branch will be
 recognized as (fun x->x), not (fun x->A). We also add a fine
 detection of inductive types with phantom type variables, for which
 this optimisation is type-unsafe.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13267 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions