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/coretactics.ml4 | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'ltac/coretactics.ml4')

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index de4d589eee..6186667584 100644
--- a/ltac/coretactics.ml4
+++ b/ltac/coretactics.ml4
@@ -151,7 +151,10 @@ END
 
 TACTIC EXTEND symmetry
   [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ]
-| [ "symmetry" clause_dft_concl(cl) ] -> [ Tactics.intros_symmetry cl ]
+END
+
+TACTIC EXTEND symmetry_in
+| [ "symmetry" "in" in_clause(cl) ] -> [ Tactics.intros_symmetry cl ]
 END
 
 (** Split *)
-- 
cgit v1.2.3