Revert "Prevent pretyping from checking well-guardedness unnecessarily."

This reverts commit 9f4e67a7c9f22ca853e76f4837a276a6111bf159.

1 files changed, 8 insertions, 3 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 94749648e0..d9f490ba55 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -73,9 +73,14 @@ let search_guard loc env possible_indexes fixdefs =
   (* We treat it separately in order to get proper error msg. *)
   let is_singleton = function [_] -> true | _ -> false in
   if List.for_all is_singleton possible_indexes then
-    (* in this case, errors are delegated to the kernel, which will
-       check well-guardedness if required. *)
-    Array.of_list (List.map List.hd possible_indexes)
+    let indexes = Array.of_list (List.map List.hd possible_indexes) in
+    let fix = ((indexes, 0),fixdefs) in
+    (try check_fix env ~chk:true fix
+     with reraise ->
+       let (e, info) = Errors.push reraise in
+       let info = Loc.add_loc info loc in
+       iraise (e, info));
+    indexes
   else
     (* we now search recursively among all combinations *)
     (try