diff options
Diffstat (limited to 'proofs/redexpr.ml')
| -rw-r--r-- | proofs/redexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 12aec9142..d0782e970 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -223,7 +223,7 @@ let subst_red_expr subs e = subst_gen_red_expr (Mod_subst.subst_mps subs) (Mod_subst.subst_evaluable_reference subs) - (Pattern.subst_pattern subs) + (Patternops.subst_pattern subs) e let inReduction : bool * string * red_expr -> obj = |