diff options
| author | Arnaud Spiwack | 2015-06-26 21:15:36 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-09-25 10:40:10 +0200 |
| commit | e0547f9e9134a9fff122df900942a094c53535c3 (patch) | |
| tree | 9b5a11a7fb28857dd26f472d6329e14a1529393a /plugins/funind | |
| parent | 576d7a815174106f337fca2f19ad7f26a7e87cc4 (diff) | |
Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming guardedness.
Diffstat (limited to 'plugins/funind')
| -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 61f03d6f22..53ec304ccc 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(None, List.map snd recsl)) + (Vernacexpr.VernacFixpoint(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 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),_,_,_,_),_) -> |