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.

0 files changed, 0 insertions, 0 deletions