aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/obligations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/obligations.ml')
-rw-r--r--toplevel/obligations.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 3d15f2142..4d8d537f2 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -567,7 +567,7 @@ let declare_mutual_definition l =
List.map3 compute_possible_guardness_evidences
wfl fixdefs fixtypes in
let indexes =
- Pretyping.search_guard ~tflags:Declareops.safe_flags
+ Pretyping.search_guard
Loc.ghost (Global.env())
possible_indexes fixdecls in
Some indexes,