Merge branch 'v8.6'

8 files changed, 44 insertions, 6 deletions

diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index b6d731f9f0..28ff6df838 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 8a316419e8..53b726432c 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' = Pltac.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
diff --git a/ltac/g_tactic.ml4 b/ltac/g_tactic.ml4
index 4e657fe831..685c07c9a8 100644
--- a/ltac/g_tactic.ml4
+++ b/ltac/g_tactic.ml4
@@ -222,7 +222,7 @@ open Vernac_
 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/ltac/pltac.ml b/ltac/pltac.ml
index fb5204d891..1d21118ae8 100644
--- a/ltac/pltac.ml
+++ b/ltac/pltac.ml
@@ -33,6 +33,7 @@ let destruction_arg = make_gen_entry utactic "destruction_arg"
 let int_or_var = make_gen_entry utactic "int_or_var"
 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/ltac/pltac.mli b/ltac/pltac.mli
index 27eb9f2804..810e1ec39a 100644
--- a/ltac/pltac.mli
+++ b/ltac/pltac.mli
@@ -29,6 +29,7 @@ val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry
 val int_or_var : int or_var 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/ltac/pptactic.ml b/ltac/pptactic.ml
index 80cafb3abd..6230fa0606 100644
--- a/ltac/pptactic.ml
+++ b/ltac/pptactic.ml
@@ -450,13 +450,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
 
@@ -470,6 +470,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) ->
@@ -486,7 +497,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/ltac/pptacticsig.mli b/ltac/pptacticsig.mli
index 455cc1be1b..74ddd377ad 100644
--- a/ltac/pptacticsig.mli
+++ b/ltac/pptacticsig.mli
@@ -27,6 +27,9 @@ module type Pp = sig
 
   val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> 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