From cc153dbbe45d5cf7f6ebfef6010adcc4f5bb568c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 2 Dec 2015 15:18:42 +0100
Subject: Dead code from August 2014 in apply in.

---
 parsing/g_tactic.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c94ac846f1..8e5e1f1fb8 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -399,7 +399,7 @@ GEXTEND Gram
       | -> [] ] ]
   ;
   in_hyp_as:
-    [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (None,id,ipat)
+    [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat)
       | -> None ] ]
   ;
   orient:
-- 
cgit v1.2.3