Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr;

petites améliorations de l'afficheur de ltac match context (moins de
parentheses, plus de structure)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8726 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 29 insertions, 8 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index e4cc3cd916..7b19b1b6c5 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -619,6 +619,8 @@ let rec strip_context n iscast t =
 let pr_constr_expr c = pr lsimple c
 let pr_lconstr_expr c = pr ltop c
 let pr_pattern_expr c = pr lsimple c
+let pr_lpattern_expr c = pr ltop c
+
 let pr_cases_pattern_expr = pr_patt ltop
 
 let pr_binders = pr_undelimited_binders (pr ltop)
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index ecfa5b4f33..5c3daa28eb 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -64,6 +64,7 @@ val pr_sort : rawsort -> std_ppcmds
 
 val pr_binders : local_binder list -> std_ppcmds
 val pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds
+val pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds
 val pr_constr_expr : constr_expr -> std_ppcmds
 val pr_lconstr_expr : constr_expr -> std_ppcmds
 val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index a90e001f5d..0657765daf 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -436,17 +436,27 @@ let pr_match_pattern pr_pat = function
   | Subterm (Some id,a) ->
       str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
 
-let pr_match_hyps pr_pat = function
-  | Hyp (nal,mp) -> pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
+let pr_match_hyps pr_pat (Hyp (nal,mp)) =
+  pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
 
 let pr_match_rule m pr pr_pat = function
   | Pat ([],mp,t) when m ->
       pr_match_pattern pr_pat mp ++
       spc () ++ str "=>" ++ brk (1,4) ++ pr t
+(*
   | Pat (rl,mp,t) ->
-      prlist_with_sep (fun () -> str",") (pr_match_hyps pr_pat) rl ++
-      spc () ++ str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
-      str "=>" ++ brk (1,4) ++ pr t
+      hv 0 (prlist_with_sep pr_coma (pr_match_hyps pr_pat) rl ++
+        (if rl <> [] then spc () else mt ()) ++ 
+         hov 0 (str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
+	 str "=>" ++ brk (1,4) ++ pr t))
+*)
+  | Pat (rl,mp,t) ->
+      hov 0 (
+	hv 0 (prlist_with_sep pr_coma (pr_match_hyps pr_pat) rl) ++
+        (if rl <> [] then spc () else mt ()) ++ 
+        hov 0 (
+	  str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++
+	  str "=>" ++ brk (1,4) ++ pr t))
   | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
 
 let pr_funvar = function
@@ -936,7 +946,7 @@ let rec raw_printers =
     (pr_raw_tactic_level, 
      drop_env pr_constr_expr,
      drop_env pr_lconstr_expr,
-     pr_pattern_expr,
+     pr_lpattern_expr,
      drop_env pr_reference,
      drop_env pr_reference,
      pr_reference,
@@ -956,7 +966,7 @@ let rec glob_printers =
     (pr_glob_tactic_level, 
      (fun env -> pr_and_constr_expr (pr_rawconstr_env env)),
      (fun env -> pr_and_constr_expr (pr_lrawconstr_env env)),
-     (fun c -> pr_constr_pattern_env (Global.env()) c),
+     (fun c -> pr_lconstr_pattern_env (Global.env()) c),
      (fun env -> pr_or_var (pr_and_short_name (pr_evaluable_reference_env env))),
      (fun env -> pr_or_var (pr_inductive env)),
      pr_ltac_or_var (pr_located pr_ltac_constant),
@@ -975,7 +985,7 @@ let ((pr_tactic_level:Environ.env -> tolerability -> Proof_type.tactic_expr -> s
     (pr_glob_tactic_level,
      pr_constr_env,
      pr_lconstr_env,
-     pr_constr_pattern,
+     pr_lconstr_pattern,
      pr_evaluable_reference_env,
      pr_inductive,
      pr_ltac_constant,
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 84aa2701ed..d6d7534955 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -77,8 +77,13 @@ let pr_rawconstr c =
 let pr_cases_pattern t =
   pr_cases_pattern_expr (extern_cases_pattern Idset.empty t)
 
+let pr_lconstr_pattern_env env c =
+  pr_lconstr_expr (extern_constr_pattern (names_of_rel_context env) c)
 let pr_constr_pattern_env env c =
   pr_constr_expr (extern_constr_pattern (names_of_rel_context env) c)
+
+let pr_lconstr_pattern t =
+  pr_lconstr_expr (extern_constr_pattern empty_names_context t)
 let pr_constr_pattern t =
   pr_constr_expr (extern_constr_pattern empty_names_context t)
 
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 5d9ea753c4..3048a7e46c 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -50,6 +50,9 @@ val pr_lrawconstr          : rawconstr -> std_ppcmds
 val pr_rawconstr_env       : env -> rawconstr -> std_ppcmds
 val pr_rawconstr           : rawconstr -> std_ppcmds
 
+val pr_lconstr_pattern_env : env -> constr_pattern -> std_ppcmds
+val pr_lconstr_pattern     : constr_pattern -> std_ppcmds
+
 val pr_constr_pattern_env  : env -> constr_pattern -> std_ppcmds
 val pr_constr_pattern      : constr_pattern -> std_ppcmds