diff options
Diffstat (limited to 'pretyping/pattern.ml')
| -rw-r--r-- | pretyping/pattern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index c3b49b9749..d64e84fea0 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -185,7 +185,7 @@ let rec subst_pattern subst pat = match pat with if c' == c && c1' == c1 && c2' == c2 then pat else PIf (c',c1',c2') | PCase ((a,b,ind,n as cs),typ,c,branches) -> - let ind' = option_smartmap (Inductiveops.subst_inductive subst) ind in + let ind' = Option.smartmap (Inductiveops.subst_inductive subst) ind in let typ' = subst_pattern subst typ in let c' = subst_pattern subst c in let branches' = array_smartmap (subst_pattern subst) branches in |