ecReduction: restore main's reduce_head Fapp(Fop) dispatch ordering

The deploy-tc rewrite of `reduce_head`'s `Fapp(Fop p, args)` case used
`find_map_opt` over `[user; delta; tc]` after `reduce_logic`, catching
only `NotRed NoHead` from each callback. This subtly differs from main
when `reduce_user_gen` succeeds: with the new layout, head reduction
fires of_realI on `of_reald (Real.inv X)`, then immediately delta-
unfolds the resulting `Rp.inv (of_reald X)` back to
`of_reald (Real.inv (to_real (of_reald X)))` — looping forever in the
RedTbl-memoized `whnf` driver because each step produces a fresh form.

Restoring main's ordering — try logic, then user_gen, and only fall
through to delta+tc when *both* raised `NoHead` — short-circuits the
loop in the cases that previously hung (split's lazy_match calls
during `auto`).

Also drops the file_exclude workaround that masked the symptom in three
ehoare examples; they all run end-to-end on the deploy-tc test runner
again.

Author: strub

config/tests.config

@@ -9,15 +9,6 @@ exclude = theories/prelude
 [test-examples]
 okdirs  = !examples
 exclude = examples/MEE-CBC examples/old examples/old/list-ddh !examples/incomplete examples/to-port !examples/tcstdlib !examples/typeclasses
-# TODO(deploy-tc): the three excluded ehoare examples expose a runaway
-# in cbv simplification when [auto.] runs t_progress on a non-PHL
-# subgoal involving xreal. The of_realI hint-simplify rule fires
-# repeatedly on cycling forms (~5 distinct hash tags) — disabling
-# of_realI removes the loop. Disabling [delta_tc] in full_red does
-# not help; the loop also persists with the merge sharing fixes
-# (see [Substitution: preserve physical sharing ...] commit).
-# adversary.ec / qselect.ec fail earlier on smt() under -script -no-eco.
-file_exclude = */ehoare/random_boolean_matrix.ec */ehoare/adversary.ec */ehoare/qselect/qselect.ec
 
 [test-mee-cbc]
 okdirs = examples/MEE-CBC

src/ecReduction.ml

@@ -1116,15 +1116,14 @@ let reduce_head simplify ri env hyps f =
         ; reduce_tc ri env ]
 
   | Fapp ({ f_node = Fop (p, _); }, args) -> begin
-    try
-      reduce_logic ri env hyps f p args
-    with NotRed _ ->
-      oget ~exn:needsubterm @@
-        List.find_map_opt
-          (fun cb -> try Some (cb f) with NotRed NoHead -> None)
-          [ reduce_user_gen simplify ri env hyps
-          ; reduce_delta ri env
-          ; reduce_tc ri env ]
+      try  reduce_logic ri env hyps f p args
+      with NotRed kind1 ->
+        try  reduce_user_gen simplify ri env hyps f
+        with NotRed kind2 ->
+          if kind1 = NoHead && kind2 = NoHead then
+            (try reduce_delta ri env f
+             with NotRed NoHead -> reduce_tc ri env f)
+          else raise needsubterm
     end
 
   | Ftuple _ -> begin