From 9bdd8aff92829aaa7c5a45b6e4e5adfa9e8789df Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 8 Oct 2016 00:10:55 +0200
Subject: Fix bug #5098: Symmetry broken in HoTT.

We defactorize the in_clause grammar entry to allow parsing of the "symmetry"
tactic when it has no arguments. Beforehand, the clause_dft_concl entry
accepted the empty stream, preventing the definition of symmetry as a mere
identifier.
---
 ltac/extraargs.ml4 | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'ltac/extraargs.ml4')

diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index c6d72e03e2..0db1cd7bae 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -260,6 +260,20 @@ END
 
 let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c
 
+let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Ppconstr.pr_lident cl
+let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl
+let in_clause' = Pcoq.Tactic.in_clause
+
+ARGUMENT EXTEND in_clause
+  TYPED AS clause_dft_concl
+  PRINTED BY pr_in_top_clause
+  RAW_TYPED AS clause_dft_concl
+  RAW_PRINTED BY pr_in_clause
+  GLOB_TYPED AS clause_dft_concl
+  GLOB_PRINTED BY pr_in_clause
+| [ in_clause'(cl) ] -> [ cl ]
+END
+
 (* spiwack: the print functions are incomplete, but I don't know what they are
 	used for *)
 let pr_r_nat_field natf =
-- 
cgit v1.2.3