Suite intégration de constr_pattern

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

4 files changed, 17 insertions, 18 deletions

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 70297f5868..b8a004a586 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -38,7 +38,7 @@ let (pattern_stock : (int list * constr_pattern) Stock.stock) =
   Stock.make_stock { name = "PATTERN"; proc = parse_pattern }
 
 let put_pat = Stock.stock pattern_stock
-let get_pat = Stock.retrieve pattern_stock
+let get_pat tm = snd (Stock.retrieve pattern_stock tm)
 
 let make_module_marker = Stock.make_module_marker
 
@@ -55,7 +55,7 @@ let (squeleton_stock : (int list * constr) Stock.stock) =
 let put_squel = Stock.stock squeleton_stock
 let get_squel_core = Stock.retrieve squeleton_stock
 
-
+(*
 let dest_somatch n pat =
   let _,m = get_pat pat in
   matches m n
@@ -71,7 +71,7 @@ let dest_somatch_conv env sigma n pat =
 let somatches_conv env sigma n pat =
   let _,m = get_pat pat in
   is_matching_conv env sigma m n
-
+*)
 let soinstance squel arglist =
   let mvs,c = get_squel_core squel in
   let mvb = List.combine mvs arglist in 
@@ -199,8 +199,8 @@ let match_with_equation  t =
         let constr_types = Global.mind_lc_without_abstractions ind in 
         let nconstr = Global.mind_nconstr ind in
 	if nconstr = 1 &&
-           (somatches constr_types.(0) refl_rel_pat1 ||
-            somatches constr_types.(0) refl_rel_pat2) 
+           (is_matching (get_pat refl_rel_pat1) constr_types.(0) ||
+            is_matching (get_pat refl_rel_pat2) constr_types.(0)) 
         then 
 	  Some (hdapp,args)
         else 
@@ -213,10 +213,10 @@ let arrow_pat = put_pat mmk "(?1 -> ?2)"
 
 let match_with_nottype t =
   try
-    let sigma = dest_somatch t arrow_pat in
-    let arg = List.assoc 1 sigma in
-    let mind = List.assoc 2 sigma in
-    if is_empty_type mind then Some (mind,arg) else None
+    match matches (get_pat arrow_pat) t with
+      |	[(1,arg);(2,mind)] ->
+	  if is_empty_type mind then Some (mind,arg) else None
+      | _ -> anomaly "Incorrect pattern matching" 
   with PatternMatchingFailure -> None  
 
 let is_nottype t = op2bool (match_with_nottype t)
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 0235fa79f2..ddba560af5 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -7,6 +7,7 @@ open Names
 open Term
 open Sign
 open Evd
+open Pattern
 open Proof_trees
 (*i*)
 
@@ -55,8 +56,7 @@ val make_module_marker : string list -> module_mark
 
 type marked_pattern
 val put_pat            : module_mark -> string -> marked_pattern
-(*val get_pat            : marked_pattern -> constr*)
-
+val get_pat            : marked_pattern -> constr_pattern
 
 (* [put_squel mmk s] declares an open term [s] to be parsed using the
    definitions in the modules associated to the key [mmk] *)
@@ -99,7 +99,6 @@ val dest_somatch : constr -> marked_pattern -> constr list
 (* [somatches c pat] just tells if [c] matches against [pat] *)
 
 val somatches    : constr -> marked_pattern -> bool
-*)
 
 (* [dest_somatch_conv env sigma] matches up to conversion in
    environment [(env,sgima)] when constants in pattern are concerned;
@@ -113,6 +112,7 @@ val dest_somatch_conv :
 
 val somatches_conv :
   Environ.env -> 'a evar_map -> constr -> marked_pattern -> bool
+*)
 
 val soinstance   : marked_term -> constr list -> constr 
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6169847c16..6e7831b1cb 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -118,13 +118,12 @@ let clause_type cls gl =
 
 (* Functions concerning matching of clausal environments *)
 
-let gl_is_matching gls pat n =
+let pf_is_matching gls pat n =
   let (wc,_) = startWalk gls in 
   is_matching_conv (w_env wc) (w_Underlying wc) pat n
 
-let gl_matches gls pat n =
-  let (wc,_)  = startWalk gls in
-  matches_conv (w_env wc) (w_Underlying wc) pat n
+let pf_matches gls pat n =
+  matches_conv (sig_it gls).Evd.evar_env (Stamps.ts_it (sig_sig gls)) pat n
 
 (* [OnCL clausefinder clausetac]
  * executes the clausefinder to find the clauses, and then executes the
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index ac118b6d1b..24b705ac72 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -52,8 +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
 *)
-val gl_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list
-val gl_is_matching : goal sigma -> constr_pattern -> constr -> bool
+val pf_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list
+val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 
 val allHyps    : goal sigma -> clause list
 val afterHyp   : identifier -> goal sigma -> clause list