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

6 files changed, 10 insertions, 9 deletions

diff --git a/tactics/auto.mli b/tactics/auto.mli
index fce449c027..d97e82df63 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -9,6 +9,7 @@ open Sign
 open Proof_trees
 open Tacmach
 open Clenv
+open Pattern
 (*i*)
   
 type auto_tactic = 
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 2d0b2f1065..d673b9316f 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -4,7 +4,7 @@
 (*i*)
 open Generic
 open Term
-open Rawterm
+open Pattern
 (*i*)
 
 (* Discrimination nets with bounded depth. *)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index ec18aa9fe4..8dc9450d1a 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -9,6 +9,7 @@ open Evd
 open Environ
 open Proof_trees
 open Tacmach
+open Hipattern
 open Pattern
 open Wcclausenv
 open Tacticals
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 5275805236..5100d6c668 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -4,7 +4,7 @@
 (*i*)
 open Generic
 open Term
-open Rawterm
+open Pattern
 (*i*)
 
 (* Named, bounded-depth, term-discrimination nets. *)
@@ -27,5 +27,5 @@ val dnet_depth : int ref
 val freeze : ('na,'a) t -> ('na,'a) frozen_t
 val unfreeze : ('na,'a) frozen_t -> ('na,'a) t -> unit
 val empty : ('na,'a) t -> unit
-val to2lists : ('na,'a) t -> ('na * (Rawterm.constr_pattern * 'a)) list * 
-                             (Rawterm.constr_label option * 'a Btermdn.t) list
+val to2lists : ('na,'a) t -> ('na * (constr_pattern * 'a)) list * 
+                             (constr_label option * 'a Btermdn.t) list
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index f863bad68a..ac118b6d1b 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -52,9 +52,8 @@ val clause_type : clause -> goal sigma -> constr
 val matches      : goal sigma -> constr -> marked_term -> bool
 val dest_match   : goal sigma -> constr -> marked_term -> constr list
 *)
-(* The second argument is the pattern *)
-val matches      : goal sigma -> constr -> marked_pattern -> bool
-val dest_match   : goal sigma -> constr -> constr -> constr list
+val gl_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list
+val gl_is_matching : goal sigma -> constr_pattern -> constr -> bool
 
 val allHyps    : goal sigma -> clause list
 val afterHyp   : identifier -> goal sigma -> clause list
@@ -83,7 +82,7 @@ val ifOnClause     :
    [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the
    right values to build a tactic *)
 
-val conclPattern : constr -> Rawterm.constr_pattern -> Coqast.t -> tactic
+val conclPattern : constr -> constr_pattern -> Coqast.t -> tactic
 
 (*s Elimination tacticals. *)
 
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index 1b8a132abf..10726df139 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -4,7 +4,7 @@
 (*i*)
 open Generic
 open Term
-open Rawterm
+open Pattern
 (*i*)
   
 (* Discrimination nets of terms. *)