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 ++++-
 ltac/extraargs.ml4   | 14 ++++++++++++++
 ltac/extraargs.mli   |  5 +++++
 3 files changed, 23 insertions(+), 1 deletion(-)

(limited to 'ltac')

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 *)
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 =
diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli
index 0cf77935c2..b12187e18a 100644
--- a/ltac/extraargs.mli
+++ b/ltac/extraargs.mli
@@ -71,3 +71,8 @@ val pr_by_arg_tac :
 
 val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
 val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type
+
+val wit_in_clause :
+  (Id.t Loc.located Locus.clause_expr,
+  Id.t Loc.located Locus.clause_expr,
+  Id.t Locus.clause_expr) Genarg.genarg_type
-- 
cgit v1.2.3