From 4d239ab9f096843dc1c78744dfc9b316ab49d6d9 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 15 Jun 2016 19:19:58 +0200 Subject: Allow `Pretyping.search_guard` to not check guard This is a minimal modification to the pretyping interface which allows for toplevel fixed points to be accepted by the pretyper. Toplevel co-fixed points are accepted without this. However (co-)fixed point _nested_ inside a `Definition` or a `Fixpoint` are always checked for guardedness by the pretyper. --- pretyping/pretyping.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/pretyping.mli') diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 142b54513..1ef3da150 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -22,7 +22,7 @@ open Misctypes (** An auxiliary function for searching for fixpoint guard indexes *) -val search_guard : +val search_guard : tflags:Declarations.typing_flags -> Loc.t -> env -> int list list -> rec_declaration -> int array type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -- cgit v1.2.3