From 64e94267cb80adc1b4df782cc83a579ee521b59b Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 5 Apr 2016 09:25:54 +0200
Subject: Revert "Prevent pretyping from checking well-guardedness
 unnecessarily."

This reverts commit 9f4e67a7c9f22ca853e76f4837a276a6111bf159.
---
 pretyping/pretyping.ml | 11 ++++++++---
 1 file 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
-- 
cgit v1.2.3