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

31 files changed, 244 insertions, 133 deletions

diff --git a/CHANGES b/CHANGES
index 3add96bc85..fac3d90343 100644
--- a/CHANGES
+++ b/CHANGES
@@ -51,6 +51,7 @@ Tactics
 - When applying a component of a conjunctive lemma, "apply in" (and
   sequences of "apply in") now leave the side conditions of the lemmas
   uniformly after the main goal (possible source of rare incompatibilities).
+- In "simpl c" and "change c with d", c can be a pattern.
 
 Tactic Language
 
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 9a71fe95b2..00836c5bee 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -78,6 +78,8 @@ Evarutil
 Term_dnet
 Recordops
 Evarconv
+Pattern
+Matching
 Tacred
 Classops
 Typeclasses_errors
@@ -89,7 +91,6 @@ Unification
 Cases
 Pretyping
 Clenv
-Pattern
 
 Lexer
 Ppextend
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e819e70099..1f6aff434c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1345,7 +1345,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
   with
       InternalisationError (loc,e) ->
 	user_err_loc (loc,"internalize",
-	  explain_internalisation_error e ++ str ".")
+	  explain_internalisation_error e)
 
 (**************************************************************************)
 (* Functions to translate constr_expr into rawconstr                       *)
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 65f0433d30..241c92582a 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -57,6 +57,8 @@ type rawconstr_and_expr = rawconstr * constr_expr option
 type open_constr_expr = unit * constr_expr
 type open_rawconstr = unit * rawconstr_and_expr
 
+type rawconstr_pattern_and_expr = rawconstr_and_expr * Pattern.constr_pattern
+
 type 'a with_ebindings = 'a * open_constr bindings
 
 (* Dynamics but tagged by a type expression *)
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 664ed43f06..fab5ff33e9 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -13,6 +13,7 @@ open Names
 open Term
 open Libnames
 open Rawterm
+open Pattern
 open Topconstr
 open Term
 open Evd
@@ -33,6 +34,8 @@ type rawconstr_and_expr = rawconstr * constr_expr option
 type open_constr_expr = unit * constr_expr
 type open_rawconstr = unit * rawconstr_and_expr
 
+type rawconstr_pattern_and_expr = rawconstr_and_expr * constr_pattern
+
 type 'a with_ebindings = 'a * open_constr bindings
 
 type intro_pattern_expr =
@@ -177,8 +180,8 @@ val rawwit_constr : (constr_expr,rlevel) abstract_argument_type
 val globwit_constr : (rawconstr_and_expr,glevel) abstract_argument_type
 val wit_constr : (constr,tlevel) abstract_argument_type
 
-val rawwit_constr_may_eval : ((constr_expr,reference or_by_notation) may_eval,rlevel) abstract_argument_type
-val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,glevel) abstract_argument_type
+val rawwit_constr_may_eval : ((constr_expr,reference or_by_notation,constr_expr) may_eval,rlevel) abstract_argument_type
+val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var,rawconstr_pattern_and_expr) may_eval,glevel) abstract_argument_type
 val wit_constr_may_eval : (constr,tlevel) abstract_argument_type
 
 val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel) abstract_argument_type
@@ -201,9 +204,9 @@ val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type
 val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type
 val wit_bindings : (constr bindings sigma,tlevel) abstract_argument_type
 
-val rawwit_red_expr : ((constr_expr,reference or_by_notation) red_expr_gen,rlevel) abstract_argument_type
-val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel) abstract_argument_type
-val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,tlevel) abstract_argument_type
+val rawwit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,rlevel) abstract_argument_type
+val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var,rawconstr_pattern_and_expr) red_expr_gen,glevel) abstract_argument_type
+val wit_red_expr : ((constr,evaluable_global_reference,constr_pattern) red_expr_gen,tlevel) abstract_argument_type
 
 val wit_list0 :
   ('a,'co) abstract_argument_type -> ('a list,'co) abstract_argument_type
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index b625480863..d724e2e737 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -224,7 +224,7 @@ module Tactic :
     val casted_open_constr : open_constr_expr Gram.Entry.e
     val constr_with_bindings : constr_expr with_bindings Gram.Entry.e
     val bindings : constr_expr bindings Gram.Entry.e
-    val constr_may_eval : (constr_expr,reference or_by_notation) may_eval Gram.Entry.e
+    val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.Entry.e
     val quantified_hypothesis : quantified_hypothesis Gram.Entry.e
     val int_or_var : int or_var Gram.Entry.e
     val red_expr : raw_red_expr Gram.Entry.e
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 4fd7390e81..7a189dbe4c 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -727,10 +727,10 @@ open Genarg
 
 let pr_metaid id = str"?" ++ pr_id id
 
-let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
+let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
   | Red false -> str "red"
   | Hnf -> str "hnf"
-  | Simpl o -> str "simpl" ++ pr_opt (pr_with_occurrences pr_constr) o
+  | Simpl o -> str "simpl" ++ pr_opt (pr_with_occurrences pr_pattern) o
   | Cbv f ->
       if f = {rBeta=true;rIota=true;rZeta=true;rDelta=true;rConst=[]} then
 	str "compute"
@@ -750,11 +750,11 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref) = function
   | ExtraRedExpr s -> str s
   | CbvVm -> str "vm_compute"
 
-let rec pr_may_eval test prc prlc pr2 = function
+let rec pr_may_eval test prc prlc pr2 pr3 = function
   | ConstrEval (r,c) ->
       hov 0
         (str "eval" ++ brk (1,1) ++
-         pr_red_expr (prc,prlc,pr2) r ++
+         pr_red_expr (prc,prlc,pr2,pr3) r ++
 	 str " in" ++ spc() ++ prc c)
   | ConstrContext ((_,id),c) ->
       hov 0
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 5767c9955c..f107d59847 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -57,11 +57,11 @@ val pr_with_occurrences :
 val pr_with_occurrences_with_trailer :
   ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds -> std_ppcmds
 val pr_red_expr :
-  ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) ->
-    ('a,'b) red_expr_gen -> std_ppcmds
+  ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
+    ('a,'b,'c) red_expr_gen -> std_ppcmds
 val pr_may_eval :
   ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
-    ('a,'b) may_eval -> std_ppcmds
+  ('c -> std_ppcmds) -> ('a,'b,'c) may_eval -> std_ppcmds
 
 val pr_rawsort : rawsort -> std_ppcmds
 
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index ad6e2c61bb..8e62c1ee2a 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -139,7 +139,7 @@ let out_bindings = function
 
 let if_pattern_ident b pr c = (if b then str "?" else mt()) ++ pr c
 
-let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argument) =
+let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
   match Genarg.genarg_tag x with
   | BoolArgType -> str (if out_gen rawwit_bool x then "true" else "false")
   | IntArgType -> int (out_gen rawwit_int x)
@@ -153,11 +153,11 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu
   | SortArgType -> pr_rawsort (out_gen rawwit_sort x)
   | ConstrArgType -> prc (out_gen rawwit_constr x)
   | ConstrMayEvalArgType ->
-      pr_may_eval prc prlc (pr_or_by_notation prref)
+      pr_may_eval prc prlc (pr_or_by_notation prref) prpat
         (out_gen rawwit_constr_may_eval x)
   | QuantHypArgType -> pr_quantified_hypothesis (out_gen rawwit_quant_hyp x)
   | RedExprArgType ->
-      pr_red_expr (prc,prlc,pr_or_by_notation prref)
+      pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat)
         (out_gen rawwit_red_expr x)
   | OpenConstrArgType b -> prc (snd (out_gen (rawwit_open_constr_gen b) x))
   | ConstrWithBindingsArgType ->
@@ -165,23 +165,24 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu
   | BindingsArgType ->
       pr_bindings_no_with prc prlc (out_gen rawwit_bindings x)
   | List0ArgType _ ->
-      hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prref)
+      hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prpat prref)
 	(fold_list0 (fun a l -> a::l) x []))
   | List1ArgType _ ->
-      hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prref)
+      hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prpat prref)
 	(fold_list1 (fun a l -> a::l) x []))
-  | OptArgType _ -> hov 0 (fold_opt (pr_raw_generic prc prlc prtac prref) (mt()) x)
+  | OptArgType _ -> hov 0 (fold_opt (pr_raw_generic prc prlc prtac prpat prref) (mt()) x)
   | PairArgType _ ->
       hov 0
         (fold_pair
-	  (fun a b -> pr_sequence (pr_raw_generic prc prlc prtac prref) [a;b])
+	  (fun a b -> pr_sequence (pr_raw_generic prc prlc prtac prpat prref)
+            [a;b])
 	  x)
   | ExtraArgType s ->
       try pi1 (Stringmap.find s !genarg_pprule) prc prlc prtac x
       with Not_found -> str "[no printer for " ++ str s ++ str "]"
 
 
-let rec pr_glob_generic prc prlc prtac x =
+let rec pr_glob_generic prc prlc prtac prpat x =
   match Genarg.genarg_tag x with
   | BoolArgType -> str (if out_gen globwit_bool x then "true" else "false")
   | IntArgType -> int (out_gen globwit_int x)
@@ -196,13 +197,13 @@ let rec pr_glob_generic prc prlc prtac x =
   | ConstrArgType -> prc (out_gen globwit_constr x)
   | ConstrMayEvalArgType ->
       pr_may_eval prc prlc
-        (pr_or_var (pr_and_short_name pr_evaluable_reference))
+        (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat
         (out_gen globwit_constr_may_eval x)
   | QuantHypArgType ->
       pr_quantified_hypothesis (out_gen globwit_quant_hyp x)
   | RedExprArgType ->
       pr_red_expr
-        (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference))
+        (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat)
         (out_gen globwit_red_expr x)
   | OpenConstrArgType b -> prc (snd (out_gen (globwit_open_constr_gen b) x))
   | ConstrWithBindingsArgType ->
@@ -210,16 +211,16 @@ let rec pr_glob_generic prc prlc prtac x =
   | BindingsArgType ->
       pr_bindings_no_with prc prlc (out_gen globwit_bindings x)
   | List0ArgType _ ->
-      hov 0 (pr_sequence (pr_glob_generic prc prlc prtac)
+      hov 0 (pr_sequence (pr_glob_generic prc prlc prtac prpat)
 	(fold_list0 (fun a l -> a::l) x []))
   | List1ArgType _ ->
-      hov 0 (pr_sequence (pr_glob_generic prc prlc prtac)
+      hov 0 (pr_sequence (pr_glob_generic prc prlc prtac prpat)
 	(fold_list1 (fun a l -> a::l) x []))
-  | OptArgType _ -> hov 0 (fold_opt (pr_glob_generic prc prlc prtac) (mt()) x)
+  | OptArgType _ -> hov 0 (fold_opt (pr_glob_generic prc prlc prtac prpat) (mt()) x)
   | PairArgType _ ->
       hov 0
         (fold_pair
-	  (fun a b -> pr_sequence (pr_glob_generic prc prlc prtac) [a;b])
+	  (fun a b -> pr_sequence (pr_glob_generic prc prlc prtac prpat) [a;b])
 	  x)
   | ExtraArgType s ->
       try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x
@@ -227,7 +228,7 @@ let rec pr_glob_generic prc prlc prtac x =
 
 open Closure
 
-let rec pr_generic prc prlc prtac x =
+let rec pr_generic prc prlc prtac prpat x =
   match Genarg.genarg_tag x with
   | BoolArgType -> str (if out_gen wit_bool x then "true" else "false")
   | IntArgType -> int (out_gen wit_int x)
@@ -243,7 +244,8 @@ let rec pr_generic prc prlc prtac x =
   | ConstrMayEvalArgType -> prc (out_gen wit_constr_may_eval x)
   | QuantHypArgType -> pr_quantified_hypothesis (out_gen wit_quant_hyp x)
   | RedExprArgType ->
-      pr_red_expr (prc,prlc,pr_evaluable_reference) (out_gen wit_red_expr x)
+      pr_red_expr (prc,prlc,pr_evaluable_reference,prpat)
+        (out_gen wit_red_expr x)
   | OpenConstrArgType b -> prc (snd (out_gen (wit_open_constr_gen b) x))
   | ConstrWithBindingsArgType ->
       let (c,b) = (out_gen wit_constr_with_bindings x).Evd.it in
@@ -251,15 +253,16 @@ let rec pr_generic prc prlc prtac x =
   | BindingsArgType ->
       pr_bindings_no_with prc prlc (out_gen wit_bindings x).Evd.it
   | List0ArgType _ ->
-      hov 0 (pr_sequence (pr_generic prc prlc prtac)
+      hov 0 (pr_sequence (pr_generic prc prlc prtac prpat)
 	(fold_list0 (fun a l -> a::l) x []))
   | List1ArgType _ ->
-      hov 0 (pr_sequence (pr_generic prc prlc prtac)
+      hov 0 (pr_sequence (pr_generic prc prlc prtac prpat)
 	(fold_list1 (fun a l -> a::l) x []))
-  | OptArgType _ -> hov 0 (fold_opt (pr_generic prc prlc prtac) (mt()) x)
+  | OptArgType _ -> hov 0 (fold_opt (pr_generic prc prlc prtac prpat) (mt()) x)
   | PairArgType _ ->
       hov 0
-        (fold_pair (fun a b -> pr_sequence (pr_generic prc prlc prtac) [a;b])
+        (fold_pair (fun a b -> pr_sequence (pr_generic prc prlc prtac prpat)
+          [a;b])
 	  x)
   | ExtraArgType s ->
       try pi3 (Stringmap.find s !genarg_pprule) prc prlc prtac x
@@ -283,12 +286,12 @@ let pr_extend_gen pr_gen lev s l =
   with Not_found ->
     str s ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
 
-let pr_raw_extend prc prlc prtac =
-  pr_extend_gen (pr_raw_generic prc prlc prtac pr_reference)
-let pr_glob_extend prc prlc prtac =
-  pr_extend_gen (pr_glob_generic prc prlc prtac)
-let pr_extend prc prlc prtac =
-  pr_extend_gen (pr_generic prc prlc prtac)
+let pr_raw_extend prc prlc prtac prpat =
+  pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
+let pr_glob_extend prc prlc prtac prpat =
+  pr_extend_gen (pr_glob_generic prc prlc prtac prpat)
+let pr_extend prc prlc prtac prpat =
+  pr_extend_gen (pr_generic prc prlc prtac prpat)
 
 (**********************************************************************)
 (* The tactic printer                                                 *)
@@ -602,8 +605,8 @@ let pr_tac_level = pr_tac_level env in
 let pr_bindings = pr_bindings pr_lconstr pr_constr in
 let pr_ex_bindings = pr_bindings_gen true pr_lconstr pr_constr in
 let pr_with_bindings = pr_with_bindings pr_lconstr pr_constr in
-let pr_extend = pr_extend pr_constr pr_lconstr pr_tac_level in
-let pr_red_expr = pr_red_expr (pr_constr,pr_lconstr,pr_cst) in
+let pr_extend = pr_extend pr_constr pr_lconstr pr_tac_level pr_pat in
+let pr_red_expr = pr_red_expr (pr_constr,pr_lconstr,pr_cst,pr_pat) in
 
 let pr_constrarg c = spc () ++ pr_constr c in
 let pr_lconstrarg c = spc () ++ pr_lconstr c in
@@ -841,7 +844,7 @@ and pr_atom1 = function
       (match occ with
           None -> mt()
         | Some occlc ->
-	    pr_with_occurrences_with_trailer pr_constr occlc
+	    pr_with_occurrences_with_trailer pr_pat occlc
 	      (spc () ++ str "with ")) ++
       pr_constr c ++ pr_clauses (Some true) pr_ident h)
 
@@ -966,7 +969,7 @@ let rec pr_tac inherited tac =
   | TacArg(ConstrMayEval (ConstrTerm c)) ->
       str "constr:" ++ pr_constr c, latom
   | TacArg(ConstrMayEval c) ->
-      pr_may_eval pr_constr pr_lconstr pr_cst c, leval
+      pr_may_eval pr_constr pr_lconstr pr_cst pr_pat c, leval
   | TacArg(TacFreshId l) -> str "fresh" ++ pr_fresh_ids l, latom
   | TacArg(Integer n) -> int n, latom
   | TacArg(TacCall(loc,f,[])) -> pr_ref f, latom
@@ -988,8 +991,7 @@ and pr_tacarg = function
   | IntroPattern ipat -> str "ipattern:" ++ pr_intro_pattern ipat
   | TacVoid -> str "()"
   | Reference r -> pr_ref r
-  | ConstrMayEval c ->
-      pr_may_eval pr_constr pr_lconstr pr_cst c
+  | ConstrMayEval c -> pr_may_eval pr_constr pr_lconstr pr_cst pr_pat c
   | TacFreshId l -> str "fresh" ++ pr_fresh_ids l
   | TacExternal (_,com,req,la) ->
       str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++
@@ -1043,7 +1045,7 @@ let rec glob_printers =
     (pr_glob_tactic_level,
      (fun env -> pr_and_constr_expr (pr_rawconstr_env env)),
      (fun env -> pr_and_constr_expr (pr_lrawconstr_env env)),
-     (fun (_,c) -> pr_lconstr_pattern_env (Global.env()) c),
+     (fun (c,_) -> pr_and_constr_expr (pr_rawconstr_env (Global.env())) c),
      (fun env -> pr_or_var (pr_and_short_name (pr_evaluable_reference_env env))),
      (fun env -> pr_or_var (pr_inductive env)),
      pr_ltac_or_var (pr_located pr_ltac_constant),
@@ -1096,3 +1098,4 @@ let _ = for i=0 to 5 do
   (globwit_tactic i, pr_tac_polymorphic i)
   (wit_tactic i, pr_tac_polymorphic i)
 done
+
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index f84a2deb27..446dc9f9d4 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -15,6 +15,7 @@ open Pretyping
 open Proof_type
 open Topconstr
 open Rawterm
+open Pattern
 open Ppextend
 open Environ
 open Evd
@@ -60,22 +61,26 @@ val pr_raw_generic :
   (constr_expr -> std_ppcmds) ->
   (constr_expr -> std_ppcmds) ->
   (tolerability -> raw_tactic_expr -> std_ppcmds) ->
+  (constr_expr -> std_ppcmds) ->
   (Libnames.reference -> std_ppcmds) -> rlevel generic_argument ->
     std_ppcmds
 
 val pr_raw_extend:
   (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) ->
-  (tolerability -> raw_tactic_expr -> std_ppcmds) -> int ->
+  (tolerability -> raw_tactic_expr -> std_ppcmds) ->
+  (constr_expr -> std_ppcmds) -> int ->
     string -> raw_generic_argument list -> std_ppcmds
 
 val pr_glob_extend:
   (rawconstr_and_expr -> std_ppcmds) -> (rawconstr_and_expr -> std_ppcmds) ->
-  (tolerability -> glob_tactic_expr -> std_ppcmds) -> int ->
+  (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+  (rawconstr_pattern_and_expr -> std_ppcmds) -> int ->
     string -> glob_generic_argument list -> std_ppcmds
 
 val pr_extend :
   (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) ->
-  (tolerability -> glob_tactic_expr -> std_ppcmds) -> int ->
+  (tolerability -> glob_tactic_expr -> std_ppcmds) ->
+  (constr_pattern -> std_ppcmds) -> int ->
     string -> typed_generic_argument list -> std_ppcmds
 
 val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 224b2e2bf9..3ef45072cc 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -69,7 +69,7 @@ let pr_gen env t =
   pr_raw_generic
     pr_constr_expr
     pr_lconstr_expr
-    (pr_raw_tactic_level env) pr_reference t
+    (pr_raw_tactic_level env) pr_constr_expr pr_reference t
 
 let pr_raw_tactic tac = pr_raw_tactic (Global.env()) tac
 
@@ -579,7 +579,7 @@ let rec pr_vernac = function
         | None -> mt()
         | Some r ->
             str"Eval" ++ spc() ++
-            pr_red_expr (pr_constr, pr_lconstr, pr_smart_global) r ++
+            pr_red_expr (pr_constr, pr_lconstr, pr_smart_global, pr_constr) r ++
             str" in" ++ spc() in
       let pr_def_body = function
         | DefineBody (bl,red,body,d) ->
@@ -890,7 +890,7 @@ let rec pr_vernac = function
       let pr_mayeval r c = match r with
       | Some r0 ->
           hov 2 (str"Eval" ++ spc() ++
-          pr_red_expr (pr_constr,pr_lconstr,pr_smart_global) r0 ++
+          pr_red_expr (pr_constr,pr_lconstr,pr_smart_global, pr_constr) r0 ++
           spc() ++ str"in" ++ spc () ++ pr_constr c)
       | None -> hov 2 (str"Check" ++ spc() ++ pr_constr c)
       in
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index e1a16ce498..2e4d07d633 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -215,9 +215,9 @@ let compute_rhs bodyi index_of_f =
           let i = destRel (array_last args) in
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
-          PApp (pattern_of_constr Evd.empty f, Array.map aux args)
+          PApp (snd (pattern_of_constr Evd.empty f), Array.map aux args)
       | Cast (c,_,_) -> aux c
-      | _ -> pattern_of_constr Evd.empty c
+      | _ -> snd (pattern_of_constr Evd.empty c)
   in
   aux bodyi
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index f1da217a60..d46fd226e9 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -658,7 +658,8 @@ let rec subst_rawconstr subst raw =
 	if ref' == ref then raw else
 	  RHole (loc,InternalHole)
   | RHole (loc, (BinderType _ | QuestionMark _ | CasesType | InternalHole |
-      TomatchTypeParameter _ | GoalEvar | ImpossibleCase)) -> raw
+      TomatchTypeParameter _ | GoalEvar | ImpossibleCase | MatchingVar _)) ->
+      raw
 
   | RCast (loc,r1,k) ->
       (match k with
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 7b8c623607..105672564f 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -92,6 +92,7 @@ let head_of_constr_reference c = match kind_of_term c with
 open Evd
 
 let pattern_of_constr sigma t =
+  let ctx = ref [] in
   let rec pattern_of_constr t =
   match kind_of_term t with
     | Rel n  -> PRel n
@@ -106,9 +107,11 @@ let pattern_of_constr sigma t =
     | App (f,a) ->
         (match 
           match kind_of_term f with
-            Evar (evk,args) ->
+            Evar (evk,args as ev) ->
               (match snd (Evd.evar_source evk sigma) with
-                  MatchingVar (true,n) -> Some n
+                  MatchingVar (true,id) ->
+                    ctx := (id,None,existential_type sigma ev)::!ctx;
+                    Some id
                 | _ -> None)
             | _ -> None
           with
@@ -117,9 +120,11 @@ let pattern_of_constr sigma t =
     | Const sp         -> PRef (ConstRef (constant_of_kn(canonical_con sp)))
     | Ind sp        -> PRef (canonical_gr (IndRef sp))
     | Construct sp -> PRef (canonical_gr (ConstructRef sp))
-    | Evar (evk,ctxt) ->
+    | Evar (evk,ctxt as ev) ->
         (match snd (Evd.evar_source evk sigma) with
-          | MatchingVar (b,n) -> assert (not b); PMeta (Some n)
+          | MatchingVar (b,id) ->
+              ctx := (id,None,existential_type sigma ev)::!ctx;
+              assert (not b); PMeta (Some id)
           | GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt)
           | _ -> PMeta None)
     | Case (ci,p,a,br) ->
@@ -129,8 +134,11 @@ let pattern_of_constr sigma t =
 	       pattern_of_constr p,pattern_of_constr a,
 	       Array.map pattern_of_constr br)
     | Fix f -> PFix f
-    | CoFix f -> PCoFix f
-  in pattern_of_constr t
+    | CoFix f -> PCoFix f in
+  let p = pattern_of_constr t in
+  (* side-effect *)
+  (* Warning: the order of dependencies in ctx is not ensured *)
+  (!ctx,p)
 
 (* To process patterns, we need a translation without typing at all. *)
 
@@ -167,7 +175,7 @@ let rec subst_pattern subst pat =
   | PRef ref ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then pat else
-	 pattern_of_constr Evd.empty t
+	 snd (pattern_of_constr Evd.empty t)
   | PVar _
   | PEvar _
   | PRel _ -> pat
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 0e87025fc8..e7460377b1 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -66,7 +66,7 @@ val head_of_constr_reference : Term.constr -> global_reference
    a pattern; currently, no destructor (Cases, Fix, Cofix) and no
    existential variable are allowed in [c] *)
 
-val pattern_of_constr : Evd.evar_map -> constr -> constr_pattern
+val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern
 
 (* [pattern_of_rawconstr l c] translates a term [c] with metavariables into
    a pattern; variables bound in [l] are replaced by the pattern to which they
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index b40476c973..e847894a53 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -11,6 +11,9 @@ Typing
 Evarutil
 Term_dnet
 Recordops
+Rawterm
+Pattern
+Matching
 Tacred
 Evarconv
 Typeclasses_errors
@@ -19,11 +22,8 @@ Classops
 Coercion
 Unification
 Clenv
-Rawterm
-Pattern
 Detyping
 Indrec
 Cases
 Pretyping
-Matching
 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 727ac117ca..16421b2a71 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -344,10 +344,10 @@ let no_occurrences_expr = (true,[])
 
 type 'a with_occurrences = occurrences_expr * 'a
 
-type ('a,'b) red_expr_gen =
+type ('a,'b,'c) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl of 'a with_occurrences option
+  | Simpl of 'c with_occurrences option
   | Cbv of 'b raw_red_flag
   | Lazy of 'b raw_red_flag
   | Unfold of 'b with_occurrences list
@@ -356,8 +356,8 @@ type ('a,'b) red_expr_gen =
   | ExtraRedExpr of string
   | CbvVm
 
-type ('a,'b) may_eval =
+type ('a,'b,'c) may_eval =
   | ConstrTerm of 'a
-  | ConstrEval of ('a,'b) red_expr_gen * 'a
+  | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
   | ConstrContext of (loc * identifier) * 'a
   | ConstrTypeOf of 'a
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 5cf227440a..ac4f0dec66 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -155,10 +155,10 @@ val no_occurrences_expr : occurrences_expr
 
 type 'a with_occurrences = occurrences_expr * 'a
 
-type ('a,'b) red_expr_gen =
+type ('a,'b,'c) red_expr_gen =
   | Red of bool
   | Hnf
-  | Simpl of 'a with_occurrences option
+  | Simpl of 'c with_occurrences option
   | Cbv of 'b raw_red_flag
   | Lazy of 'b raw_red_flag
   | Unfold of 'b with_occurrences list
@@ -167,8 +167,8 @@ type ('a,'b) red_expr_gen =
   | ExtraRedExpr of string
   | CbvVm
 
-type ('a,'b) may_eval =
+type ('a,'b,'c) may_eval =
   | ConstrTerm of 'a
-  | ConstrEval of ('a,'b) red_expr_gen * 'a
+  | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
   | ConstrContext of (loc * identifier) * 'a
   | ConstrTypeOf of 'a
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 7079b937b1..a103c49b61 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -23,6 +23,8 @@ open Closure
 open Reductionops
 open Cbv
 open Rawterm
+open Pattern
+open Matching
 
 (* Errors *)
 
@@ -733,10 +735,10 @@ let simpl env sigma c = strong whd_simpl env sigma c
 
 (* Reduction at specific subterms *)
 
-let is_head c t =
+let matches_head c t =
   match kind_of_term t with
-    | App (f,_) -> f = c
-    | _ -> false
+    | App (f,_) -> matches c f
+    | _ -> raise PatternMatchingFailure
 
 let contextually byhead ((nowhere_except_in,locs),c) f env sigma t =
   let maxocc = List.fold_right max locs 0 in
@@ -744,22 +746,23 @@ let contextually byhead ((nowhere_except_in,locs),c) f env sigma t =
   let rec traverse (env,c as envc) t =
     if nowhere_except_in & (!pos > maxocc) then t
     else
-    if (not byhead & eq_constr c t) or (byhead & is_head c t) then
+    try
+      let subst = if byhead then matches_head c t else matches c t in
       let ok =
 	if nowhere_except_in then List.mem !pos locs
 	else not (List.mem !pos locs) in
       incr pos;
       if ok then
-	f env sigma t
+	f subst env sigma t
       else if byhead then
 	(* find other occurrences of c in t; TODO: ensure left-to-right *)
         let (f,l) = destApp t in
 	mkApp (f, array_map_left (traverse envc) l)
       else
 	t
-    else
+    with PatternMatchingFailure ->
       map_constr_with_binders_left_to_right
-	(fun d (env,c) -> (push_rel d env,lift 1 c))
+	(fun d (env,c) -> (push_rel d env,lift_pattern 1 c))
         traverse envc t
   in
   let t' = traverse (env,c) t in
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 80eca2bcc5..2bba87a75e 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -17,6 +17,7 @@ open Reductionops
 open Closure
 open Rawterm
 open Termops
+open Pattern
 (*i*)
 
 type reduction_tactic_error =
@@ -92,5 +93,5 @@ val reduce_to_quantified_ref :
 val reduce_to_atomic_ref :
   env ->  evar_map -> Libnames.global_reference -> types -> types
 
-val contextually : bool -> occurrences * constr -> reduction_function
-  -> reduction_function
+val contextually : bool -> occurrences * constr_pattern ->
+  (patvar_map -> reduction_function) -> reduction_function
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
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0e4091b3cb..8447dfdef6 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -273,7 +273,7 @@ let make_exact_entry sigma pri (c,cty) =
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = Pattern.pattern_of_constr sigma cty in
+	let pat = snd (Pattern.pattern_of_constr sigma cty) in
 	let head = 
 	  try head_of_constr_reference (fst (head_constr cty)) 
 	  with _ -> failwith "make_exact_entry" 
@@ -287,7 +287,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
     | Prod _ ->
         let ce = mk_clenv_from dummy_goal (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = Pattern.pattern_of_constr sigma c' in
+	let pat = snd (Pattern.pattern_of_constr sigma c') in
         let hd = (try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry") in
         let nmiss = List.length (clenv_missing ce) in
@@ -354,7 +354,7 @@ let make_trivial env sigma c =
   let hd = head_of_constr_reference (fst (head_constr t)) in
   let ce = mk_clenv_from dummy_goal (c,t) in
   (Some hd, { pri=1;
-         pat = Some (Pattern.pattern_of_constr sigma (clenv_type ce));
+         pat = Some (snd (Pattern.pattern_of_constr sigma (clenv_type ce)));
          code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) })
 
 open Vernacexpr
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 70eb8dfb30..d649c8b315 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -108,7 +108,8 @@ val h_simplest_right  : tactic
 (* Conversion *)
 val h_reduce          : Redexpr.red_expr -> Tacticals.clause -> tactic
 val h_change          :
-  constr with_occurrences option -> constr -> Tacticals.clause -> tactic
+  Pattern.constr_pattern with_occurrences option -> constr -> 
+    Tacticals.clause -> tactic
 
 (* Equivalence relations *)
 val h_reflexivity     : tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f031df2560..719fa7f859 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -575,13 +575,27 @@ let intern_flag ist red =
 
 let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c)
 
+let intern_constr_pattern ist ltacvars pc =
+  let metas,pat =
+    Constrintern.intern_constr_pattern ist.gsigma ist.genv ~ltacvars pc in
+  let c = intern_constr_gen true false ist pc in
+  metas,(c,pat)
+
+let intern_typed_pattern_with_occurrences ist (l,p) =
+  let c = intern_constr_gen true false ist p in
+  (* we cannot ensure in non strict mode that the pattern is closed *)
+  (* keeping a constr_expr copy is too complicated and we want anyway to *)
+  (* type it, so we remember the pattern as a rawconstr only *)
+  let dummy_pat = PRel 0 in
+  (l,(c,dummy_pat))
+
 let intern_red_expr ist = function
   | Unfold l -> Unfold (List.map (intern_unfold ist) l)
   | Fold l -> Fold (List.map (intern_constr ist) l)
   | Cbv f -> Cbv (intern_flag ist f)
   | Lazy f -> Lazy (intern_flag ist f)
   | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l)
-  | Simpl o -> Simpl (Option.map (intern_constr_with_occurrences ist) o)
+  | Simpl o -> Simpl (Option.map (intern_typed_pattern_with_occurrences ist) o)
   | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r
 
 let intern_in_hyp_as ist lf (id,ipat) =
@@ -607,14 +621,12 @@ let intern_hyp_location ist (((b,occs),id),hl) =
 let intern_pattern ist ?(as_type=false) lfun = function
   | Subterm (b,ido,pc) ->
       let ltacvars = (lfun,[]) in
-      let (metas,pat) = intern_constr_pattern ist.gsigma ist.genv ~ltacvars pc in
-      let c = intern_constr_gen true false ist pc in
-      ido, metas, Subterm (b,ido,(c,pat))
+      let (metas,pc) = intern_constr_pattern ist ltacvars pc in
+      ido, metas, Subterm (b,ido,pc)
   | Term pc ->
       let ltacvars = (lfun,[]) in
-      let (metas,pat) = intern_constr_pattern ist.gsigma ist.genv ~as_type ~ltacvars pc in
-      let c = intern_constr_gen true false ist pc in
-      None, metas, Term (c,pat)
+      let (metas,pc) = intern_constr_pattern ist ltacvars pc in
+      None, metas, Term pc
 
 let intern_constr_may_eval ist = function
   | ConstrEval (r,c) -> ConstrEval (intern_red_expr ist r,intern_constr ist c)
@@ -782,13 +794,17 @@ let rec intern_atomic lf ist x =
   (* Conversion *)
   | TacReduce (r,cl) ->
       TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl)
-  | TacChange (occl,c,cl) ->
-      TacChange (Option.map (intern_constr_with_occurrences ist) occl,
-        (if occl = None & (cl.onhyps = None or cl.onhyps = Some []) &
+  | TacChange (None,c,cl) ->
+      TacChange (None,
+        (if (cl.onhyps = None or cl.onhyps = Some []) &
 	    (cl.concl_occs = all_occurrences_expr or
 	     cl.concl_occs = no_occurrences_expr)
          then intern_type ist c else intern_constr ist c),
 	clause_app (intern_hyp_location ist) cl)
+  | TacChange (Some occl,c,cl) ->
+      let occl = intern_typed_pattern_with_occurrences ist occl in
+      TacChange (Some occl,intern_constr ist c,
+	clause_app (intern_hyp_location ist) cl)
 
   (* Equivalence relations *)
   | TacReflexivity -> TacReflexivity
@@ -1314,7 +1330,7 @@ let solve_remaining_evars fail_evar use_classes env initial_sigma evd c =
   (* Side-effect *)
   !evdref,c
 
-let interp_gen kind ist expand_evar fail_evar use_classes env sigma (c,ce) =
+let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma (c,ce) =
   let (ltacvars,unbndltacvars as vars),typs =
     extract_ltac_vars_data ist sigma env in
   let c = match ce with
@@ -1324,7 +1340,8 @@ let interp_gen kind ist expand_evar fail_evar use_classes env sigma (c,ce) =
        intros/lettac/inversion hypothesis names *)
   | Some c ->
       let ltacdata = (List.map fst ltacvars,unbndltacvars) in
-      intern_gen (kind = IsType) ~ltacvars:ltacdata sigma env c in
+      intern_gen (kind = IsType) ~allow_patvar ~ltacvars:ltacdata sigma env c
+  in
   let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in
   let evd,c =
     catch_error trace
@@ -1339,20 +1356,22 @@ let interp_gen kind ist expand_evar fail_evar use_classes env sigma (c,ce) =
 
 (* Interprets a constr; expects evars to be solved *)
 let interp_constr_gen kind ist env sigma c =
-  snd (interp_gen kind ist true true true env sigma c)
+  snd (interp_gen kind ist false true true true env sigma c)
 
 let interp_constr = interp_constr_gen (OfType None)
 
 let interp_type = interp_constr_gen IsType
 
 (* Interprets an open constr *)
-let interp_open_constr_gen kind ist = interp_gen kind ist true false false
+let interp_open_constr_gen kind ist =
+  interp_gen kind ist false true false false
 
 let interp_open_constr ccl =
   interp_open_constr_gen (OfType ccl)
 
 let interp_typed_pattern ist env sigma c =
-  let sigma, c = interp_gen (OfType None) ist false false false env sigma c in
+  let sigma, c =
+    interp_gen (OfType None) ist true false false false env sigma c in
   pattern_of_constr sigma c
 
 (* Interprets a constr expression casted by the current goal *)
@@ -1402,11 +1421,15 @@ let interp_unfold ist env (occs,qid) =
 let interp_flag ist env red =
   { red with rConst = List.map (interp_evaluable ist env) red.rConst }
 
-let interp_pattern ist sigma env (occs,c) =
+let interp_constr_with_occurrences ist sigma env (occs,c) =
   (interp_occurrences ist occs, interp_constr ist sigma env c)
 
-let pf_interp_constr_with_occurrences ist gl =
-  interp_pattern ist (pf_env gl) (project gl)
+let interp_typed_pattern_with_occurrences ist env sigma (occs,(c,_)) =
+  let sign,p = interp_typed_pattern ist env sigma c in
+  sign, (interp_occurrences ist occs, p)
+
+let interp_closed_typed_pattern_with_occurrences ist env sigma occl =
+  snd (interp_typed_pattern_with_occurrences ist env sigma occl)
 
 let interp_constr_with_occurrences_and_name_as_list =
   interp_constr_in_compound_list
@@ -1414,7 +1437,7 @@ let interp_constr_with_occurrences_and_name_as_list =
     (function ((occs,c),Anonymous) when occs = all_occurrences_expr -> c
       | _ -> raise Not_found)
     (fun ist env sigma (occ_c,na) ->
-      sigma, (interp_pattern ist env sigma occ_c,
+      sigma, (interp_constr_with_occurrences ist env sigma occ_c,
        interp_fresh_name ist env na))
 
 let interp_red_expr ist sigma env = function
@@ -1422,8 +1445,10 @@ let interp_red_expr ist sigma env = function
   | Fold l -> Fold (List.map (interp_constr ist env sigma) l)
   | Cbv f -> Cbv (interp_flag ist env f)
   | Lazy f -> Lazy (interp_flag ist env f)
-  | Pattern l -> Pattern (List.map (interp_pattern ist env sigma) l)
-  | Simpl o -> Simpl (Option.map (interp_pattern ist env sigma) o)
+  | Pattern l ->
+      Pattern (List.map (interp_constr_with_occurrences ist env sigma) l)
+  | Simpl o ->
+      Simpl(Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
   | (Red _ |  Hnf | ExtraRedExpr _ | CbvVm as r) -> r
 
 let pf_interp_red_expr ist gl = interp_red_expr ist (project gl) (pf_env gl)
@@ -1641,9 +1666,9 @@ let use_types = false
 
 let eval_pattern lfun ist env sigma (c,pat) =
   if use_types then
-    interp_typed_pattern ist env sigma c
+    snd (interp_typed_pattern ist env sigma c)
   else
-    let lvar = List.map (fun (id,c) -> (id,lazy(pattern_of_constr Evd.empty c))) lfun in
+    let lvar = List.map (fun (id,c) -> (id,lazy(snd (pattern_of_constr Evd.empty c)))) lfun in
     instantiate_pattern lvar pat
 
 let read_pattern lfun ist env sigma = function
@@ -1768,6 +1793,12 @@ let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c)
 
 let pack_sigma (sigma,c) = {it=c;sigma=sigma}
 
+let extend_gl_hyps gl sign =
+ { gl with
+   it = { gl.it with
+     evar_hyps = 
+     List.fold_right Environ.push_named_context_val sign gl.it.evar_hyps } }
+
 (* Interprets an l-tac expression into a value *)
 let rec val_interp ist gl (tac:glob_tactic_expr) =
 
@@ -2363,14 +2394,20 @@ and interp_atomic ist gl tac =
   (* Conversion *)
   | TacReduce (r,cl) ->
       h_reduce (pf_interp_red_expr ist gl r) (interp_clause ist gl cl)
-  | TacChange (occl,c,cl) ->
-      h_change (Option.map (pf_interp_constr_with_occurrences ist gl) occl)
-        (if occl = None & (cl.onhyps = None or cl.onhyps = Some []) &
+  | TacChange (None,c,cl) ->
+      h_change None
+        (if (cl.onhyps = None or cl.onhyps = Some []) &
 	    (cl.concl_occs = all_occurrences_expr or
 	     cl.concl_occs = no_occurrences_expr)
 	 then pf_interp_type ist gl c
 	 else pf_interp_constr ist gl c)
         (interp_clause ist gl cl)
+  | TacChange (Some occl,c,cl) ->
+      let sign,occl =
+        interp_typed_pattern_with_occurrences ist env sigma occl in
+      h_change (Some occl)
+        (pf_interp_constr ist (extend_gl_hyps gl sign) c)
+        (interp_clause ist gl cl)
 
   (* Equivalence relations *)
   | TacReflexivity -> h_reflexivity
@@ -2589,13 +2626,16 @@ let subst_flag subst red =
 
 let subst_constr_with_occurrences subst (l,c) = (l,subst_rawconstr subst c)
 
+let subst_pattern_with_occurrences subst (l,(c,p)) =
+  (l,(subst_rawconstr subst c,subst_pattern subst p))
+
 let subst_redexp subst = function
   | Unfold l -> Unfold (List.map (subst_unfold subst) l)
   | Fold l -> Fold (List.map (subst_rawconstr subst) l)
   | Cbv f -> Cbv (subst_flag subst f)
   | Lazy f -> Lazy (subst_flag subst f)
   | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l)
-  | Simpl o -> Simpl (Option.map (subst_constr_with_occurrences subst) o)
+  | Simpl o -> Simpl (Option.map (subst_pattern_with_occurrences subst) o)
   | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r
 
 let subst_raw_may_eval subst = function
@@ -2687,7 +2727,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Conversion *)
   | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
   | TacChange (occl,c,cl) ->
-      TacChange (Option.map (subst_constr_with_occurrences subst) occl,
+      TacChange (Option.map (subst_pattern_with_occurrences subst) occl,
         subst_rawconstr subst c, cl)
 
   (* Equivalence relations *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 332e93c8c6..4157d332b8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -311,7 +311,9 @@ let change_and_check cv_pb t env sigma c =
 (* Use cumulativity only if changing the conclusion not a subterm *)
 let change_on_subterm cv_pb t = function
   | None -> change_and_check cv_pb t
-  | Some occl -> contextually false occl (change_and_check Reduction.CONV t)
+  | Some occl ->
+      contextually false occl
+        (fun subst -> change_and_check Reduction.CONV (replace_vars subst t))
 
 let change_in_concl occl t =
   reduct_in_concl ((change_on_subterm Reduction.CUMUL t occl),DEFAULTcast)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d2cbeb8560..e8662a50d4 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -27,6 +27,7 @@ open Genarg
 open Tacexpr
 open Nametab
 open Rawterm
+open Pattern
 open Termops
 (*i*)
 
@@ -125,8 +126,9 @@ type tactic_reduction = env -> evar_map -> constr -> constr
 val reduct_in_hyp     : tactic_reduction -> hyp_location -> tactic
 val reduct_option     : tactic_reduction * cast_kind -> goal_location -> tactic
 val reduct_in_concl   : tactic_reduction * cast_kind -> tactic
-val change_in_concl   : (occurrences * constr) option -> constr -> tactic
-val change_in_hyp     : (occurrences * constr) option -> constr ->
+val change_in_concl   : (occurrences * constr_pattern) option -> constr -> 
+                        tactic
+val change_in_hyp     : (occurrences * constr_pattern) option -> constr ->
                         hyp_location -> tactic
 val red_in_concl      : tactic
 val red_in_hyp        : hyp_location -> tactic
@@ -148,7 +150,7 @@ val unfold_in_hyp     :
 val unfold_option     :
   (occurrences * evaluable_global_reference) list -> goal_location -> tactic
 val change            :
-  (occurrences * constr) option -> constr -> clause -> tactic
+  (occurrences * constr_pattern) option -> constr -> clause -> tactic
 val pattern_option    :
   (occurrences * constr) list -> goal_location -> tactic
 val reduce            : red_expr -> clause -> tactic
diff --git a/test-suite/output/simpl.out b/test-suite/output/simpl.out
new file mode 100644
index 0000000000..73888da9a0
--- /dev/null
+++ b/test-suite/output/simpl.out
@@ -0,0 +1,15 @@
+1 subgoal
+  
+  x : nat
+  ============================
+   x = S x
+1 subgoal
+  
+  x : nat
+  ============================
+   0 + x = S x
+1 subgoal
+  
+  x : nat
+  ============================
+   x = 1 + x
diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v
new file mode 100644
index 0000000000..5f1926f142
--- /dev/null
+++ b/test-suite/output/simpl.v
@@ -0,0 +1,13 @@
+(* Simpl with patterns *)
+
+Goal forall x, 0+x = 1+x.
+intro x.
+simpl (_ + x).
+Show.
+Undo.
+simpl (_ + x) at 2.
+Show.
+Undo.
+simpl (0 + _).
+Show.
+Undo.
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index cea017122e..c72ee875af 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -4,3 +4,9 @@ Goal let a := 0+0 in a=a.
 intro.
 change 0 in (value of a).
 change ((fun A:Type => A) nat) in (type of a).
+Abort.
+
+Goal forall x, 2 + S x = 1 + S x.
+intro. 
+change (?u + S x) with (S (u + x)). 
+Abort.