From 2f3db0b605b3aa345c1fea26c263ba6793a0fa51 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 17 Jan 2019 16:17:41 +0100
Subject: [ssr] compile "=> {} y" as "=> {y} y"

---
 plugins/ssr/ssripats.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'plugins')

diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 7f8825b89f..ce5fccec96 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -529,6 +529,8 @@ let tclCompileIPats l =
       (IOpView(Some [],v)) :: elab rest
   | (IPatClear cl) :: (IPatView v) :: rest ->
       (IOpView(None,v)) :: IOpClear cl :: elab rest
+  | (IPatClear []) :: (IPatId id) :: rest ->
+      (IOpClear [SsrHyp(None,id)]) :: IOpId id :: elab rest
 
   (* boring code *)
   | [] -> []
-- 
cgit v1.2.3