diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 53ec304cc..91fcb3f8b 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -166,7 +166,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(true,None, List.map snd recsl)) + (Vernacexpr.VernacFixpoint({Declarations.check_guarded=true},None, List.map snd recsl)) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 5c849ba41..0ea90ecd1 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),_,_,_,_),_) -> |