Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour les metavariables de patterns; réparation local défs récursive dans ltac

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

2 files changed, 19 insertions, 7 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 92feaa7de7..a3b430c7d9 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -527,6 +527,16 @@ let pr_lconstr_env env c = pr ltop (transf env c)
 let pr_constr c = pr_constr_env (Global.env()) c
 let pr_lconstr c = pr_lconstr_env (Global.env()) c
 
+let transf_pattern env c =
+  if Options.do_translate() then
+    Constrextern.extern_rawconstr (Termops.vars_of_env env)
+      (Constrintern.for_grammar
+	(Constrintern.interp_rawconstr_gen false Evd.empty env [] None ([],[]))
+	c)
+  else c
+
+let pr_pattern c = pr lsimple (transf_pattern (Global.env()) c)
+
 let pr_rawconstr_env env c =
   pr_constr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c)
 let pr_lrawconstr_env env c =
@@ -547,7 +557,6 @@ let pr_binders l =
 
 let pr_cases_pattern = pr_patt ltop
 
-let pr_pattern = pr_constr
 let pr_occurrences prc (nl,c) =
   prlist (fun n -> int n ++ spc ()) nl ++
   str"(" ++ prc c ++ str")"
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 3f268fe691..67d6638a07 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -39,6 +39,10 @@ let pr_quantified_hypothesis = function
 
 let pr_quantified_hypothesis_arg h = spc () ++ pr_quantified_hypothesis h
 
+let pr_or_metanum pr = function
+  | AN x -> pr x
+  | MetaNum (_,n) -> Pattern.pr_patvar n
+
 (*
 let pr_binding prc = function
   | NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
@@ -108,8 +112,7 @@ let pr_match_pattern pr_pat = function
   | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pat a ++ str "]"
 
 let pr_match_hyps pr_pat = function
-  | NoHypId mp -> str "_:" ++ pr_match_pattern pr_pat mp
-  | Hyp ((_,id),mp) -> pr_id id ++ str ":" ++ pr_match_pattern pr_pat mp
+  | Hyp ((_,na),mp) -> pr_name na ++ str ":" ++ pr_match_pattern pr_pat mp
 
 let pr_match_rule m pr pr_pat = function
   | Pat ([],mp,t) when m ->
@@ -137,15 +140,15 @@ let pr_let_clause k pr prc pr_cst = function
 let pr_let_clauses pr prc pr_cst = function
   | hd::tl ->
       hv 0
-        (pr_let_clause "let " pr prc pr_cst hd ++ spc () ++
-         prlist_with_sep spc (pr_let_clause "with " pr prc pr_cst) tl)
+        (pr_let_clause "let " pr prc pr_cst hd ++
+         prlist (fun t -> spc () ++ pr_let_clause "with " pr prc pr_cst t) tl)
   | [] -> anomaly "LetIn must declare at least one binding"
 
 let pr_rec_clause pr ((_,id),(l,t)) =
-  pr_id id ++ prlist pr_funvar l ++ str "=>" ++ spc () ++ pr t
+  hov 0 (pr_id id ++ prlist pr_funvar l ++ str " :=") ++ spc () ++ pr t
 
 let pr_rec_clauses pr l = 
-  prlist_with_sep (fun () -> fnl () ++ str "and ") (pr_rec_clause pr) l
+  prlist_with_sep (fun () -> fnl () ++ str "with ") (pr_rec_clause pr) l
 
 let pr_hintbases = function
   | None -> spc () ++ str "with *"