From d4f3a1a807d474050a4e91e16ff7813f1db7f537 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 7 Jun 2016 09:52:43 +0200
Subject: Assume totality: dedicated type rather than bool

The rational is that

1. further typing flags may be available in the future
2. it makes it easier to trace and document the argument
---
 intf/vernacexpr.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ba9ac16b60..2f2f973761 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -307,10 +307,10 @@ type vernac_expr =
       bool (*[false] => assume positive*) *
       private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
-      bool * (* [false] => assume guarded *)
+      Declarations.typing_flags *
       locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
-      bool * (* [false] => assume guarded *)
+      Declarations.typing_flags *
       locality option * (cofixpoint_expr * decl_notation list) list
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
-- 
cgit v1.2.3