diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-01-21 18:45:36 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-01-21 23:56:01 +0100 |
| commit | 176d8e004153e65688dc8ef4f22f7939fd6101b1 (patch) | |
| tree | 1a5343064619e3442c4cc0cb8da4e103167dc743 /tactics/inv.ml | |
| parent | be0eca32fae93ed4793c2f839bb9e725b6a963d1 (diff) | |
New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).
- Fixing dead code, doc.
- Relaxing constraints on using an as-tuple in inversion.
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 8030fc32e..ded1e8076 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -296,8 +296,8 @@ let get_names (allow_conj,issimple) (loc, pat as x) = match pat with error "Discarding pattern not allowed for inversion equations." | 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 [] | IntroOrPattern [[]])) when allow_conj -> (None, []) + | 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 |