diff options
| -rw-r--r-- | tactics/inv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 9bfbbc41b7..6841ab0ecd 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -298,7 +298,7 @@ let get_names (allow_conj,issimple) (loc, pat as x) = match pat with | IntroAction (IntroRewrite _) -> error "Rewriting pattern not allowed for inversion equations." | IntroAction (IntroOrAndPattern (IntroAndPattern [])) when allow_conj -> (None, []) - | IntroAction (IntroOrAndPattern (IntroAndPattern ((_,IntroNaming (IntroIdentifier id)) :: _ as l))) + | IntroAction (IntroOrAndPattern (IntroAndPattern ((_,IntroNaming (IntroIdentifier id)) :: _ as l) | IntroOrPattern [(_,IntroNaming (IntroIdentifier id)) :: _ as l ])) when allow_conj -> (Some id,l) | IntroAction (IntroOrAndPattern (IntroAndPattern _)) -> if issimple then |