From 7c598f9f1f6da2cecc70557f9f436392322fc6d9 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 2 Apr 2019 01:47:11 +0200
Subject: [ssr] under: use varnames from the 1st ipat with multi-goal under
 lemmas

In particular, this enhances support for lemma eq_big (with 2 side-conditions).
---
 plugins/ssr/ssrfwd.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 349f0082e1..b5082582c9 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -403,7 +403,10 @@ let undertac ist ipats ((dir,_),_ as rule) hint =
       | IPatAnon (One _ | Drop) :: rest ->
           aux (Names.Name.Anonymous :: acc) rest
       | _ -> List.rev acc in
-    aux [] (Option.default [] ipats) in
+    aux [] @@ match ipats with
+              | None -> []
+              | Some (IPatCase(Regular (l :: _)) :: _) -> l
+              | Some l -> l in
 
   (* If we find a "=> [|]" we add 1 | to get "=> [||]" for the extra
    * goal (the one that is left once we run over) *)
-- 
cgit v1.2.3