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@383 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 35 insertions, 34 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 7d9d3530a..f0b4e81ad 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -11,6 +11,7 @@ open Inductive
 open Evd
 open Reduction
 open Typing
+open Pattern
 open Tacmach
 open Proof_trees
 open Pfedit
@@ -702,7 +703,7 @@ let possible_resolve db_list local_db cl =
 let decomp_unary_term c gls = 
   let typc = pf_type_of gls c in 
   let hd = List.hd (head_constr typc) in 
-  if Pattern.is_conjunction hd then 
+  if Hipattern.is_conjunction hd then 
     simplest_case c gls 
   else 
     errorlabstrm "Auto.decomp_unary_term" [<'sTR "not a unary type" >] 
@@ -710,7 +711,7 @@ let decomp_unary_term c gls =
 let decomp_empty_term c gls = 
   let typc = pf_type_of gls c in 
   let (hd,_) = decomp_app typc in 
-  if Pattern.is_empty_type hd then 
+  if Hipattern.is_empty_type hd then 
     simplest_case c gls 
   else 
     errorlabstrm "Auto.decomp_empty_term" [<'sTR "not an empty type" >] 
@@ -858,7 +859,7 @@ let compileAutoArg contac = function
 	 tclFIRST 
            (List.map2 
               (fun id typ -> 
-                 if (Pattern.is_conjunction (hd_of_prod typ)) then 
+                 if (Hipattern.is_conjunction (hd_of_prod typ)) then 
 		   (tclTHEN
                       (tclTHEN (simplest_elim (mkVar id)) 
                          (clear_one id))
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 3dbbacea6..e238f5f79 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -3,7 +3,7 @@
 
 open Term
 open Termdn
-open Rawterm
+open Pattern
 
 (* Discrimination nets with bounded depth.
    See the module dn.ml for further explanations.
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 0ca3f6b2a..a21b3e6d7 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -128,8 +128,8 @@ open Pcoq
 
 (* two patterns - one for the type, and one for the type of the type *)
 type destructor_pattern = {
-  d_typ: Rawterm.constr_pattern; 
-  d_sort: Rawterm.constr_pattern }
+  d_typ: constr_pattern; 
+  d_sort: constr_pattern }
     
 type ('a,'b) location = Hyp of 'a | Concl of 'b
 
@@ -222,11 +222,11 @@ let _ =
 	     add_destructor_hint na
                (match loc with
 		  | Hyp b ->
-		      Hyp(b,{d_typ=pat;d_sort=PMeta(new_meta())},
-			  { d_typ=PMeta(new_meta());
-		       	    d_sort=PMeta(new_meta()) })
+		      Hyp(b,{d_typ=pat;d_sort=PMeta(Some (new_meta()))},
+			  { d_typ=PMeta(Some (new_meta()));
+		       	    d_sort=PMeta(Some (new_meta())) })
 		  | Concl () ->
-		      Concl({d_typ=pat;d_sort=PMeta(new_meta())}))
+		      Concl({d_typ=pat;d_sort=PMeta(Some (new_meta()))}))
                pri code
        | _ -> bad_vernac_args "HintDestruct")
 
@@ -234,13 +234,13 @@ let match_dpat dp cls gls =
   let cltyp = clause_type cls gls in
   match (cls,dp) with
     | (Some id,Hyp(_,hypd,concld)) ->
-        (somatch None hypd.d_typ cltyp)@
-        (somatch None hypd.d_sort (pf_type_of gls cltyp))@
-        (somatch None concld.d_typ (pf_concl gls))@
-        (somatch None concld.d_sort (pf_type_of gls (pf_concl gls)))
+        (matches hypd.d_typ cltyp)@
+        (matches hypd.d_sort (pf_type_of gls cltyp))@
+        (matches concld.d_typ (pf_concl gls))@
+        (matches concld.d_sort (pf_type_of gls (pf_concl gls)))
     | (None,Concl concld) ->
-        (somatch None concld.d_typ (pf_concl gls))@
-        (somatch None concld.d_sort (pf_type_of gls (pf_concl gls)))
+        (matches concld.d_typ (pf_concl gls))@
+        (matches concld.d_sort (pf_type_of gls (pf_concl gls)))
     | _ -> error "ApplyDestructor"
 
 let applyDestructor cls discard dd gls =
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 69c4104d9..4abff0e4d 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -9,7 +9,7 @@ open Term
 open Reduction
 open Proof_trees
 open Clenv
-open Pattern
+open Hipattern
 open Tacmach
 open Tacticals
 open Tactics
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ff62150a0..e1fe98148 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -18,6 +18,7 @@ open Proof_trees
 open Logic
 open Wcclausenv
 open Pattern
+open Hipattern
 open Tacticals
 open Tactics
 open Tacinterp
@@ -526,12 +527,12 @@ let rec build_discriminator sigma env dirn c sort = function
   | _ -> assert false
 
 let dest_somatch_eq eqn eq_pat =
-  match dest_somatch eqn eq_pat with
+  match matches eqn eq_pat with
     | [t;x;y] -> (t,x,y)
     | _ -> anomaly "dest_somatch_eq: an eq pattern should match 3 terms"
 	  
 let find_eq_data_decompose eqn =
-  if (somatches eqn eq_pattern) then
+  if (matches eqn eq_pattern) then
     (eq, dest_somatch_eq eqn eq_pattern)
   else if (somatches eqn eqT_pattern) then
     (eqT, dest_somatch_eq eqn eqT_pattern)
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index e762531d4..09b772950 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -7,6 +7,7 @@ open Generic
 open Term
 open Libobject
 open Library
+open Pattern
 
 (* Named, bounded-depth, term-discrimination nets.
    Implementation:
@@ -20,12 +21,12 @@ open Library
    Eduardo (5/8/97) *)
 
 type ('na,'a) t = {
-  mutable table : ('na,Rawterm.constr_pattern * 'a) Gmap.t;
-  mutable patterns : (Rawterm.constr_label option,'a Btermdn.t) Gmap.t }
+  mutable table : ('na,constr_pattern * 'a) Gmap.t;
+  mutable patterns : (constr_label option,'a Btermdn.t) Gmap.t }
 
 type ('na,'a) frozen_t = 
-    ('na,Rawterm.constr_pattern * 'a) Gmap.t
-    * (Rawterm.constr_label option,'a Btermdn.t) Gmap.t
+    ('na,constr_pattern * 'a) Gmap.t
+    * (constr_label option,'a Btermdn.t) Gmap.t
 
 let create () =
   { table = Gmap.empty;
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6425bdc28..6169847c1 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -118,16 +118,13 @@ let clause_type cls gl =
 
 (* Functions concerning matching of clausal environments *)
 
-let matches gls n pat =
+let gl_is_matching gls pat n =
   let (wc,_) = startWalk gls in 
-  somatches_conv (w_env wc) (w_Underlying wc) n pat
+  is_matching_conv (w_env wc) (w_Underlying wc) pat n
 
-let dest_match gls n m =
-  let mvs     = collect_metas m in
+let gl_matches gls pat n =
   let (wc,_)  = startWalk gls in
-  let (mvb,_) = Clenv.unify_0 [] wc m n in 
-  List.map (fun x -> List.assoc x mvb) mvs
-
+  matches_conv (w_env wc) (w_Underlying wc) pat n
 
 (* [OnCL clausefinder clausetac]
  * executes the clausefinder to find the clauses, and then executes the
@@ -191,10 +188,11 @@ si après Intros la conclusion matche le pattern.
 *)
 
 let conclPattern concl pat tacast gl = 
-  let constr_bindings = Pattern.somatch None pat concl in
+  let constr_bindings = Pattern.matches pat concl in
   let ast_bindings = 
     List.map 
-      (fun (i,c) -> (i, Termast.bdize false (assumptions_for_print []) c))
+      (fun (i,c) ->
+	 (i, Termast.ast_of_constr false (assumptions_for_print []) c))
       constr_bindings in 
   let tacast' = Coqast.subst_meta ast_bindings tacast in
   Tacinterp.interp tacast' gl
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0bc6860b2..66dd8b1ad 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -19,7 +19,7 @@ open Proof_trees
 open Logic
 open Clenv
 open Tacticals
-open Pattern
+open Hipattern
 
 exception Bound
 
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 957543e16..ec621c4a7 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -5,7 +5,7 @@ open Util
 open Generic
 open Names
 open Term
-open Rawterm
+open Pattern
 
 (* Discrimination nets of terms.
    See the module dn.ml for further explanations.