Reorganisation of intropattern code

- emphasizing the different kinds of patterns
- factorizing code of the non-naming intro-patterns

Still some questions:

- Should -> and <- apply to hypotheses or not (currently they apply to
  hypotheses either when used in assert-style tactics or apply in, or
  when the term to rewrite is a variable, in which case "subst" is
  applied)?
- Should "subst" be used when the -> or <- rewrites an equation x=t
  posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)?
- Should -> and <- be applicable in non assert-style if the lemma has
  quantifications?

3 files changed, 26 insertions, 19 deletions

diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index 3a0f7a8f7..3193a74a0 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -12,17 +12,23 @@ open Pp
 (** Printing of [intro_pattern] *)
 
 let rec pr_intro_pattern (_,pat) = match pat with
+  | IntroForthcoming true -> str "*"
+  | IntroForthcoming false -> str "**"
+  | IntroNaming p -> pr_intro_pattern_naming p
+  | IntroAction p -> pr_intro_pattern_action p
+
+and pr_intro_pattern_naming = function
+  | IntroWildcard -> str "_"
+  | IntroIdentifier id -> Nameops.pr_id id
+  | IntroFresh id -> str "?" ++ Nameops.pr_id id
+  | IntroAnonymous -> str "?"
+
+and pr_intro_pattern_action = function
   | IntroOrAndPattern pll -> pr_or_and_intro_pattern pll
   | IntroInjection pl ->
       str "[=" ++ hv 0 (prlist_with_sep spc pr_intro_pattern pl) ++ str "]"
-  | IntroWildcard -> str "_"
   | IntroRewrite true -> str "->"
   | IntroRewrite false -> str "<-"
-  | IntroIdentifier id -> Nameops.pr_id id
-  | IntroFresh id -> str "?" ++ Nameops.pr_id id
-  | IntroForthcoming true -> str "*"
-  | IntroForthcoming false -> str "**"
-  | IntroAnonymous -> str "?"
 
 and pr_or_and_intro_pattern = function
   | [pl] ->
diff --git a/printing/miscprint.mli b/printing/miscprint.mli
index 4e0be83f2..d242bad3a 100644
--- a/printing/miscprint.mli
+++ b/printing/miscprint.mli
@@ -12,6 +12,10 @@ open Misctypes
 
 val pr_intro_pattern : intro_pattern_expr Loc.located -> Pp.std_ppcmds
 
+val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
+
+val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds
+
 (** Printing of [move_location] *)
 
 val pr_move_location :
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 785b0e8dc..3caee02de 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -347,26 +347,23 @@ let pr_bindings prc prlc = pr_bindings_gen false prc prlc
 let pr_with_bindings prc prlc (c,bl) =
   hov 1 (prc c ++ pr_bindings prc prlc bl)
 
-let pr_as_ipat pat = str "as " ++ Miscprint.pr_intro_pattern pat
-let pr_eqn_ipat pat = str "eqn:" ++ Miscprint.pr_intro_pattern pat
+let pr_as_disjunctive_ipat (_,ipatl) =
+  str "as " ++ Miscprint.pr_or_and_intro_pattern ipatl
+let pr_eqn_ipat (_,ipat) = str "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat
+let pr_as_ipat = function
+  | None -> mt ()
+  | Some ipat -> str "as " ++ Miscprint.pr_intro_pattern ipat
 
 let pr_with_induction_names = function
   | None, None -> mt ()
   | Some eqpat, None -> spc () ++ hov 1 (pr_eqn_ipat eqpat)
-  | None, Some ipat -> spc () ++ hov 1 (pr_as_ipat ipat)
+  | None, Some ipat -> spc () ++ hov 1 (pr_as_disjunctive_ipat ipat)
   | Some eqpat, Some ipat ->
-    spc () ++ hov 1 (pr_as_ipat ipat ++ spc () ++ pr_eqn_ipat eqpat)
-
-let pr_as_intro_pattern ipat =
-  spc () ++ hov 1 (str "as" ++ spc () ++ Miscprint.pr_intro_pattern ipat)
+    spc () ++ hov 1 (pr_as_disjunctive_ipat ipat ++ spc () ++ pr_eqn_ipat eqpat)
 
 let pr_with_inversion_names = function
   | None -> mt ()
-  | Some ipat -> pr_as_intro_pattern ipat
-
-let pr_as_ipat = function
-  | None -> mt ()
-  | Some ipat -> pr_as_intro_pattern ipat
+  | Some ipat -> pr_as_disjunctive_ipat ipat
 
 let pr_as_name = function
   | Anonymous -> mt ()
@@ -390,7 +387,7 @@ let pr_assertion prc _prlc ipat c = match ipat with
 let pr_assumption prc prlc ipat c = match ipat with
 (* Use this "optimisation" or use only the general case ?*)
 (* it seems that this "optimisation" is somehow more natural *)
-  | Some (_,IntroIdentifier id) ->
+  | Some (_,IntroNaming (IntroIdentifier id)) ->
       spc() ++ surround (pr_id id ++ str " :" ++ spc() ++ prlc c)
   | ipat ->
       spc() ++ prc c ++ pr_as_ipat ipat