diff options
Diffstat (limited to 'toplevel/obligations.ml')
| -rw-r--r-- | toplevel/obligations.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 9df5a411ba..ec58392d51 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -582,7 +582,8 @@ let declare_mutual_definition l = List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in let indexes = - Pretyping.search_guard Loc.ghost (Global.env()) + Pretyping.search_guard ~tflags:{Declarations.check_guarded=true} + Loc.ghost (Global.env()) possible_indexes fixdecls in Some indexes, List.map_i (fun i _ -> |