The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi Laurent,

  You'll solve the complexity problem and will typecheck your example
in a few seconds if you replace in your file the expressions of the
form

      let r1 := make_PExpr_aux p1 e n in
        let r2 := make_PExpr_aux p2 e (snd r1) in
          (mkPEadd (fst r1) (fst r2), (snd r2))

by

      let (r11,r12) := make_PExpr_aux p1 e n in
        let (r21,r22) := make_PExpr_aux p2 e r12 in
          (mkPEadd r11 r21, r22)

that avoids exponential duplication of the expressions "make_PExpr_aux
x y z" when normalizing "test_in e e1".

  On the type-checking strategy question, Coq has to reduce in general
the argument of a match/if as it can potentially give informations on
the structural decreasing of the fixpoint definition. In the case of
"if", the branches does not extract information from the matched term,
so an optimization could have been done to avoid the reduction of
"test_in e e1".

  Hugo