Implementing postponed constraints in TC resolution

A constraint can be stuck if it does not match any of the declared modes
for its head (if there are any). In that case, the subgoal is postponed
and the next ones are tried. We do a fixed point computation until there
are no stuck subgoals or the set does not change (it is impossible to
make it grow, as asserted in the code, because it is always a subset of
the initial goals)

This allows constraints on classes with modes to be treated as if they were
in any order (yay for stability of solutions!). Also, ultimately it should
free us to launch resolutions more agressively (avoiding issues like the
ones seen in PR #10762).

Add more examples of the semantics of TC resolution with apply in test-suite

Properly catch ModeMatchFailure on calls to map_e*

Add fixed bug 9058 to the test-suite

Close #9058

Add documentation

Fixes after Gaëtan's review.

Main change is to not use exceptions for control-flow

Update tactics/class_tactics.ml

Clearer and more efficient mode mismatch dispatch

Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

Remove exninfo argument

1 files changed, 8 insertions, 3 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 1dde820075..d68f9271ec 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -303,7 +303,9 @@ let hintmap_of sigma secvars hdc concl =
   | None -> Hint_db.map_none ~secvars
   | Some hdc ->
      if occur_existential sigma concl then
-       Hint_db.map_existential sigma ~secvars hdc concl
+       (fun db -> match Hint_db.map_existential sigma ~secvars hdc concl db with
+                  | ModeMatch l -> l
+                  | ModeMismatch -> [])
      else Hint_db.map_auto sigma ~secvars hdc concl
 
 let exists_evaluable_reference env = function
@@ -366,11 +368,14 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
           let st = Hint_db.transparent_state db in
           let flags, l =
             let l =
-              match hdc with None -> Hint_db.map_none ~secvars db
+              match hdc with
+              | None -> Hint_db.map_none ~secvars db
               | Some hdc ->
                   if TransparentState.is_empty st
                   then Hint_db.map_auto sigma ~secvars hdc concl db
-                  else Hint_db.map_existential sigma ~secvars hdc concl db
+                  else match Hint_db.map_existential sigma ~secvars hdc concl db with
+                      | ModeMatch l -> l
+                      | ModeMismatch -> []
             in auto_flags_of_state st, l
           in List.map (fun x -> (Some flags,x)) l)
         (local_db::db_list)