From e0547f9e9134a9fff122df900942a094c53535c3 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 26 Jun 2015 21:15:36 +0200
Subject: Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control
 assuming guardedness.

---
 plugins/funind/indfun.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind/indfun.ml')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 5dcb0c0439..5c849ba415 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -399,7 +399,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        evd,List.rev rev_pconstants
     | _ ->
-       Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+       Command.do_fixpoint ~chkguard:true Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
 	   (fun (evd,l) (((_,fname),_,_,_,_),_) ->
-- 
cgit v1.2.3


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
---
 plugins/funind/indfun.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind/indfun.ml')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 5c849ba415..0ea90ecd12 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -399,7 +399,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        evd,List.rev rev_pconstants
     | _ ->
-       Command.do_fixpoint ~chkguard:true Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+       Command.do_fixpoint ~flags:{Declarations.check_guarded=true} Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
 	   (fun (evd,l) (((_,fname),_,_,_,_),_) ->
-- 
cgit v1.2.3