diff --git a/src/context_map.ml b/src/context_map.ml
index 965034cc..25b833b3 100644
--- a/src/context_map.ml
+++ b/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 CErrors.is_sync_anomaly e ->
          errorlabstrm
            (str"Type error while building context map: " ++ pr_context_map env evars map ++
             spc () ++ str"Anomaly: " ++ CErrors.print e)
diff --git a/src/equations_common.ml b/src/equations_common.ml
index 089cb1e2..ede6d685 100644
--- a/src/equations_common.ml
+++ b/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_sync_anomaly e then Relevant
 	  else raise e
   in
   let nf_qvar q = match UState.nf_qvar uctx q with
@@ -1030,7 +1030,6 @@ let user_err_loc (loc, pp) =
   CErrors.user_err ?loc pp
 let error s = CErrors.user_err (str s)
 let errorlabstrm msg = CErrors.user_err msg
-let is_anomaly = CErrors.is_anomaly
 let print_error e = CErrors.print e
 
 let nf_betadeltaiota = nf_all
diff --git a/src/equations_common.mli b/src/equations_common.mli
index ea8bdd29..66be2b93 100644
--- a/src/equations_common.mli
+++ b/src/equations_common.mli
@@ -375,7 +375,6 @@ 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 print_error : exn -> Pp.t
 val anomaly : ?label:string -> Pp.t -> 'a