--Tre the expected branching with the actual one and

--Tre the expected branching with the actual one and
       prune the candidate when the latter is larger. The optimization
              is meant to rule out stange applications of flexible terms,
                     such as the application of eq_f that always succeeds.
                            There is some gain but less than expected

                            :his line, and those below, will be ignored--

M    ng_tactics/nnAuto.ml