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.

8 files changed, 44 insertions, 6 deletions

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index de4d589ee..618666758 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 c6d72e03e..0db1cd7ba 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 0cf77935c..b12187e18 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
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 199ef9fce..3152afb28 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -220,7 +220,7 @@ let warn_deprecated_eqn_syntax =
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
   bindings red_expr int_or_var open_constr uconstr
-  simple_intropattern clause_dft_concl hypident destruction_arg;
+  simple_intropattern in_clause clause_dft_concl hypident destruction_arg;
 
   int_or_var:
     [ [ n = integer  -> ArgArg n
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 4e069c9e3..9e9a7e723 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -350,6 +350,7 @@ module Tactic =
     let red_expr = make_gen_entry utactic "red_expr"
     let simple_intropattern =
       make_gen_entry utactic "simple_intropattern"
+    let in_clause = make_gen_entry utactic "in_clause"
     let clause_dft_concl = 
       make_gen_entry utactic "clause"
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7f49c997f..7f6caf63f 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -193,6 +193,7 @@ module Tactic :
     val red_expr : raw_red_expr Gram.entry
     val simple_tactic : raw_tactic_expr Gram.entry
     val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry
+    val in_clause : Names.Id.t Loc.located Locus.clause_expr Gram.entry
     val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry
     val tactic_arg : raw_tactic_arg Gram.entry
     val tactic_expr : raw_tactic_expr Gram.entry
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index f3117db17..1e618b59e 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -583,13 +583,13 @@ module Make
     | None -> mt()
 
   let pr_hyp_location pr_id = function
-    | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
+    | occs, InHyp -> pr_with_occurrences pr_id occs
     | occs, InHypTypeOnly ->
-      spc () ++ pr_with_occurrences (fun id ->
+      pr_with_occurrences (fun id ->
         str "(" ++ keyword "type of" ++ spc () ++ pr_id id ++ str ")"
       ) occs
     | occs, InHypValueOnly ->
-      spc () ++ pr_with_occurrences (fun id ->
+      pr_with_occurrences (fun id ->
         str "(" ++ keyword "value of" ++ spc () ++ pr_id id ++ str ")"
       ) occs
 
@@ -603,6 +603,17 @@ module Make
     | None -> mt ()
     | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
 
+  let pr_in_clause pr_id = function
+    | { onhyps=None; concl_occs=NoOccurrences } ->
+      (str "* |-")
+    | { onhyps=None; concl_occs=occs } ->
+      (pr_with_occurrences (fun () -> str "*") (occs,()))
+    | { onhyps=Some l; concl_occs=NoOccurrences } ->
+      prlist_with_sep (fun () -> str ", ") (pr_hyp_location pr_id) l
+    | { onhyps=Some l; concl_occs=occs } ->
+      let pr_occs = pr_with_occurrences (fun () -> str" |- *") (occs,()) in
+      (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs)
+
   let pr_clauses default_is_concl pr_id = function
     | { onhyps=Some []; concl_occs=occs }
         when (match default_is_concl with Some true -> true | _ -> false) ->
@@ -619,7 +630,7 @@ module Make
         | _ -> pr_with_occurrences (fun () -> str" |- *") (occs,())
       in
       pr_in
-        (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++ pr_occs)
+        (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs)
 
   let pr_orient b = if b then mt () else str "<- "
 
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index c08d6044d..665e055f2 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -29,6 +29,9 @@ module type Pp = sig
   val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
   val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
 
+  val pr_in_clause :
+    ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+
   val pr_clauses :  bool option ->
     ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds