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.

2 files changed, 18 insertions, 4 deletions

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index f3117db170..1e618b59eb 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 c08d6044db..665e055f23 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