Adapt to rocq-prover/rocq#21254 (stop catching async exceptions)

Author: SkySkimmer

src/context_map.ml

@@ -223,7 +223,7 @@ let check_ctx_map ?(unsafe = false) env evars map =
          errorlabstrm
            (str"Type error while building context map: " ++ pr_context_map env evars map ++
             spc () ++ str"Invalid_argument: " ++ str s)
-       | e when is_anomaly e ->
+       | e when is_anomaly ~async:false e ->
          errorlabstrm
            (str"Type error while building context map: " ++ pr_context_map env evars map ++
             spc () ++ str"Anomaly: " ++ CErrors.print e)

src/equations_common.ml

@@ -224,7 +224,7 @@ let collapse_term_qualities uctx c =
       | Relevant | Irrelevant as r -> r
       | RelevanceVar _ -> (* hack *) Relevant
     with e ->
-	  if CErrors.is_anomaly e then Relevant
+          if CErrors.is_anomaly ~async:false e then Relevant
 	  else raise e
   in
   let nf_qvar q = match UState.nf_qvar uctx q with

src/equations_common.mli

@@ -375,7 +375,7 @@ val pp : Pp.t -> unit
 val user_err_loc : (Loc.t option * Pp.t) -> 'a
 val error : string -> 'a
 val errorlabstrm : Pp.t -> 'a
-val is_anomaly : exn -> bool
+val is_anomaly : async:bool -> exn -> bool
 val print_error : exn -> Pp.t
 val anomaly : ?label:string -> Pp.t -> 'a