In "simpl c" and "change c with d", c can be a pattern.

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

3 files changed, 16 insertions, 12 deletions

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 287794bff9..fa6a6f3ec2 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -15,6 +15,7 @@ open Term
 open Declarations
 open Libnames
 open Rawterm
+open Pattern
 open Reductionops
 open Tacred
 open Closure
@@ -106,8 +107,8 @@ let _ =
 
 (* Generic reduction: reduction functions used in reduction tactics *)
 
-type red_expr = (constr, evaluable_global_reference) red_expr_gen
-
+type red_expr =
+    (constr, evaluable_global_reference, constr_pattern) red_expr_gen
 
 let make_flag_constant = function
   | EvalVarRef id -> fVAR id
@@ -132,8 +133,7 @@ let make_flag f =
 	  f.rConst red
   in red
 
-let is_reference c =
-  try let _ref = global_of_constr c in true with _ -> false
+let is_reference = function PRef _ | PVar _ -> true | _ -> false
 
 let red_expr_tab = ref Stringmap.empty
 
@@ -157,7 +157,8 @@ let reduction_of_red_expr = function
       else (red_product,DEFAULTcast)
   | Hnf -> (hnf_constr,DEFAULTcast)
   | Simpl (Some (_,c as lp)) ->
-    (contextually (is_reference c) (out_with_occurrences lp) simpl,DEFAULTcast)
+    (contextually (is_reference c) (out_with_occurrences lp)
+      (fun _ -> simpl),DEFAULTcast)
   | Simpl None -> (simpl,DEFAULTcast)
   | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast)
   | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast)
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index 70db56c486..63237aa209 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -11,12 +11,13 @@
 open Names
 open Term
 open Closure
+open Pattern
 open Rawterm
 open Reductionops
 open Termops
 
-
-type red_expr = (constr, evaluable_global_reference) red_expr_gen
+type red_expr =
+    (constr, evaluable_global_reference, constr_pattern) red_expr_gen
 
 val out_with_occurrences : 'a with_occurrences -> occurrences * 'a
 
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 04b7a225c7..d16ad78bac 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -204,8 +204,8 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
   | TacConstructor of evars_flag * int or_metaid * 'constr bindings
 
   (* Conversion *)
-  | TacReduce of ('constr,'cst) red_expr_gen * 'id gclause
-  | TacChange of 'constr with_occurrences option * 'constr * 'id gclause
+  | TacReduce of ('constr,'cst,'pat) red_expr_gen * 'id gclause
+  | TacChange of 'pat with_occurrences option * 'constr * 'id gclause
 
   (* Equivalence relations *)
   | TacReflexivity
@@ -259,7 +259,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg =
   | TacDynamic     of loc * Dyn.t
   | TacVoid
   | MetaIdArg      of loc * bool * string
-  | ConstrMayEval  of ('constr,'cst) may_eval
+  | ConstrMayEval  of ('constr,'cst,'pat) may_eval
   | IntroPattern   of intro_pattern_expr located
   | Reference      of 'ref
   | Integer        of int
@@ -313,7 +313,8 @@ type raw_tactic_arg =
 
 type raw_generic_argument = rlevel generic_argument
 
-type raw_red_expr = (constr_expr, reference or_by_notation) red_expr_gen
+type raw_red_expr =
+    (constr_expr, reference or_by_notation, constr_expr) red_expr_gen
 
 type glob_atomic_tactic_expr =
     (rawconstr_and_expr,
@@ -338,7 +339,8 @@ type glob_tactic_arg =
 type glob_generic_argument = glevel generic_argument
 
 type glob_red_expr =
-    (rawconstr_and_expr, evaluable_global_reference or_var) red_expr_gen
+    (rawconstr_and_expr, evaluable_global_reference or_var, constr_pattern)
+    red_expr_gen
 
 type typed_generic_argument = tlevel generic_argument