aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/functional_principles_proofs.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
-rw-r--r--plugins/funind/functional_principles_proofs.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 5bf772fc5..a3bb2eee9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -397,9 +397,9 @@ let isLetIn t =
let h_reduce_with_zeta =
h_reduce
- (Glob_term.Cbv
- {Glob_term.all_flags
- with Glob_term.rDelta = false;
+ (Genredexpr.Cbv
+ {Redops.all_flags
+ with Genredexpr.rDelta = false;
})