diff options
| author | Arnaud Spiwack | 2015-09-25 09:27:50 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-09-25 10:41:41 +0200 |
| commit | 9f4e67a7c9f22ca853e76f4837a276a6111bf159 (patch) | |
| tree | 4182e452507cf90835b448a4f8f07cf1b4685acb | |
| parent | e8bad8abc7be351a34fdf9770409bbab14bcd6a9 (diff) | |
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.
| -rw-r--r-- | pretyping/pretyping.ml | 11 |
1 files 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 |