From 82e4e8f2afbff4f1dbecb8a37e3c1c18a41c754f Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Thu, 18 Feb 2016 17:32:15 +0100
Subject: FIX: of my previous merging mistake

---
 tactics/inv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3