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
---
 parsing/g_vernac.ml4 | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ced2da7a52..3ad5e77fcf 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -219,13 +219,13 @@ GEXTEND Gram
 	  let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
           VernacInductive (check_positivity a,priv,f,indl)
       | "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (check_guardedness a,None, recs)
+          VernacFixpoint ({Declarations.check_guarded=check_guardedness a},None, recs)
       | IDENT "Let"; "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (check_guardedness a,Some Discharge, recs)
+          VernacFixpoint ({Declarations.check_guarded=check_guardedness a},Some Discharge, recs)
       | "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint (check_guardedness a,None, corecs)
+          VernacCoFixpoint ({Declarations.check_guarded=check_guardedness a},None, corecs)
       | IDENT "Let"; "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint (check_guardedness a,Some Discharge, corecs)
+          VernacCoFixpoint ({Declarations.check_guarded=check_guardedness a},Some Discharge, corecs)
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l
       | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
 	      l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l)
-- 
cgit v1.2.3