Déplacement du type reference dans Term

Découpage de tactics/pattern en proofs/pattern et tactics/hipattern
Renommage des fonctions somatch and co dans Pattern et Tacticals
Divers extensions pour utiliser les constr_pattern


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

4 files changed, 26 insertions, 15 deletions

diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 70e7ab7a30..1383dc655f 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -8,6 +8,7 @@ open Sign
 open Evd
 open Environ
 open Rawterm
+open Pattern
 (*i*)
 
 (* Translation from AST to terms. *)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 1cc5ceca55..4ab8b33ac2 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -49,7 +49,7 @@ GEXTEND Gram
             <:ast< (PRODLIST $c [$id1][$id2]($SLAM $idl $body)) >>
       | "("; lc1 = lconstr; ")" -> lc1
       | "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" ->
-          <:ast< (XTRA"$SOAPP" $lc1 ($LIST $cl)) >>
+          <:ast< (SOAPP $lc1 ($LIST $cl)) >>
       | IDENT "Fix"; id = ident; "{"; fbinders = fixbinders; "}" ->
           <:ast< (FIX $id ($LIST $fbinders)) >>
       | IDENT "CoFix"; id = ident; "{"; fbinders = cofixbinders; "}" ->
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 40a1bdad3b..d6e785c8f4 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -6,12 +6,11 @@ open Pp
 open Names
 open Term
 open Sign
+open Rawterm
+open Pattern
 (*i*)
 
 (* These are the entry points for printing terms, context, tac, ... *)
-val gencompr  : path_kind -> Coqast.t -> std_ppcmds
-val gentermpr : path_kind -> 'a assumptions -> constr -> std_ppcmds
-val gentermpr_at_top : path_kind -> 'a assumptions -> constr -> std_ppcmds
 val gentacpr  : Coqast.t -> std_ppcmds
 
 val prterm_env      : 'a assumptions -> constr -> std_ppcmds
@@ -19,19 +18,17 @@ val prterm_env_at_top : 'a assumptions -> constr -> std_ppcmds
 val prterm          : constr -> std_ppcmds
 val prtype_env      : 'a assumptions -> typed_type -> std_ppcmds
 val prtype          : typed_type -> std_ppcmds
-val fprterm_env     : 'a assumptions -> constr -> std_ppcmds
-val fprterm         : constr -> std_ppcmds
-val fprtype_env     : 'a assumptions -> typed_type -> std_ppcmds
-val fprtype         : typed_type -> std_ppcmds
 
-val prrawterm       : Rawterm.rawconstr -> std_ppcmds
-val prpattern       : Rawterm.cases_pattern -> std_ppcmds
+val pr_rawterm       : Rawterm.rawconstr -> std_ppcmds
+val pr_cases_pattern : Rawterm.cases_pattern -> std_ppcmds
 
 val pr_constant     : constant -> std_ppcmds
 val pr_existential  : existential -> std_ppcmds
 val pr_constructor  : constructor -> std_ppcmds
 val pr_inductive    : inductive -> std_ppcmds
-val pr_ref_label    : Rawterm.constr_label -> std_ppcmds
+val pr_ref_label    : constr_label -> std_ppcmds
+val pr_pattern      : constr_pattern -> std_ppcmds
+val pr_pattern_env  : 'a assumptions -> constr_pattern -> std_ppcmds
 
 val pr_ne_env       : std_ppcmds -> path_kind -> context -> std_ppcmds
 
@@ -41,6 +38,12 @@ val pr_env_opt      : context -> std_ppcmds
 val emacs_str       : string -> string
 
 (* For compatibility *)
-val fterm0          : 'a assumptions -> constr -> std_ppcmds
 val term0           : 'a assumptions -> constr -> std_ppcmds
 
+val fprterm_env     : 'a assumptions -> constr -> std_ppcmds
+val fprterm         : constr -> std_ppcmds
+val fprtype_env     : 'a assumptions -> typed_type -> std_ppcmds
+val fprtype         : typed_type -> std_ppcmds
+
+(* For compatibility *)
+val fterm0          : 'a assumptions -> constr -> std_ppcmds
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 516856bcd9..064dc8c25b 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -6,13 +6,20 @@ open Names
 open Term
 open Sign
 open Rawterm
+open Pattern
 (*i*)
 
-(* Translation of pattern, rawterm and term into syntax trees for printing *)
+(* Translation of pattern, cases pattern, rawterm and term into syntax
+   trees for printing *)
 
-val ast_of_pattern : cases_pattern -> Coqast.t
+val ast_of_cases_pattern : cases_pattern -> Coqast.t
 val ast_of_rawconstr : rawconstr -> Coqast.t
-val bdize : bool -> unit assumptions -> constr -> Coqast.t
+val ast_of_pattern : unit assumptions -> constr_pattern -> Coqast.t
+
+(* If [b=true] in [ast_of_constr b env c] then the variables in the first 
+   level of quantification clashing with the variables in [env] are renamed *)
+
+val ast_of_constr : bool -> unit assumptions -> constr -> Coqast.t
 
 (*i C'est bdize qui sait maintenant s'il faut afficher les casts ou pas
 val bdize_no_casts : bool -> unit assumptions -> constr -> Coqast.t