diff options
| author | Erik Martin-Dorel | 2019-04-02 01:47:11 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 12:54:44 +0200 |
| commit | 7c598f9f1f6da2cecc70557f9f436392322fc6d9 (patch) | |
| tree | fb6c51e64a2ad97ddd8d7007c259c7a9c91ea80b /plugins | |
| parent | e68bccba9344c1b3d77d3e815af6cce1ce50b731 (diff) | |
[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).
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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) *) |