From 9f4e67a7c9f22ca853e76f4837a276a6111bf159 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 25 Sep 2015 09:27:50 +0200
Subject: Prevent pretyping from checking well-guardedness unnecessarily.

The `search_guard` function is called to infer the recursive argument of fixpoints. For each potential argument, it tests whether it is called structurally, calling the kernel test. When a single argument is available either because `{struct x}` was specified, or because there is a single inductive argument, the kernel test is performed, despite the fact that the kernel will do it later, and the kernel error reraised. It is unnecessary.
---
 pretyping/pretyping.ml | 11 +++--------
 1 file changed, 3 insertions(+), 8 deletions(-)

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d9f490ba55..94749648e0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -73,14 +73,9 @@ 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
-    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
+    (* 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)
   else
     (* we now search recursively among all combinations *)
     (try
-- 
cgit v1.2.3