diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-18 17:32:15 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-02-18 17:32:45 +0100 |
| commit | 82e4e8f2afbff4f1dbecb8a37e3c1c18a41c754f (patch) | |
| tree | aa8ed063c3cb2e7bf2ea88784a08a72e88800187 /tactics/inv.ml | |
| parent | e4c9dfe7277ec2e2c4b1e40f60044ba4cade8e61 (diff) | |
FIX: of my previous merging mistake
Diffstat (limited to 'tactics/inv.ml')
| -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 9bfbbc41b..6841ab0ec 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 |