Ajout Simpl et Change sur des sous-termes

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

3 files changed, 23 insertions, 10 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 341752f458..5cfc324eb7 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -139,6 +139,12 @@ GEXTEND Gram
     [ [ id = base_ident -> NamedHyp id
       | n = natural -> AnonHyp n ] ]
   ;
+  conversion:
+    [ [ nl = LIST1 integer; c1 = constr; "with"; c2 = constr ->
+         (Some (nl,c1), c2)
+      |	c1 = constr; "with"; c2 = constr -> (Some ([],c1), c2)
+      | c = constr -> (None, c) ] ]
+  ;
   pattern_occ:
     [ [ nl = LIST0 integer; c = constr -> (nl,c) ] ]
   ;
@@ -195,7 +201,7 @@ GEXTEND Gram
   red_tactic:
     [ [ IDENT "Red" -> Red false
       | IDENT "Hnf" -> Hnf
-      | IDENT "Simpl" -> Simpl
+      | IDENT "Simpl"; po = OPT pattern_occ -> Simpl po
       | IDENT "Cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
       | IDENT "Lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
       | IDENT "Compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta])
@@ -207,7 +213,7 @@ GEXTEND Gram
   red_expr:
     [ [ IDENT "Red" -> Red false
       | IDENT "Hnf" -> Hnf
-      | IDENT "Simpl" -> Simpl
+      | IDENT "Simpl"; po = OPT pattern_occ -> Simpl po
       | IDENT "Cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
       | IDENT "Lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
       | IDENT "Compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta])
@@ -346,7 +352,7 @@ GEXTEND Gram
       (* Conversion *)
       | r = red_tactic; cl = clause -> TacReduce (r, cl)
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
-      | IDENT "Change"; c = constr; cl = clause -> TacChange (c,cl)
+      | IDENT "Change"; (oc,c) = conversion; cl = clause -> TacChange (oc,c,cl)
 
 (* Unused ??
       | IDENT "ML"; s = string -> ExtraTactic<:ast< (MLTACTIC $s) >>
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 6571e0af8a..6c45c9e70a 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -124,6 +124,9 @@ let pr_clause_pattern pr_id = function (* To check *)
 	  ++ spc () ++ pr_id id) l ++
         pr_opt (prlist_with_sep spc int) glopt
 
+let pr_subterms pr occl =
+  hov 0 (pr_occurrences pr occl ++ spc () ++ str "with")
+
 let pr_induction_arg prc = function
   | ElimOnConstr c -> prc c
   | ElimOnIdent (_,id) -> pr_id id
@@ -452,8 +455,9 @@ and pr_atom1 = function
   (* Conversion *)  
   | TacReduce (r,h) ->
       hov 1 (pr_red_expr (pr_constr,pr_cst) r ++ pr_clause pr_ident h)
-  | TacChange (c,h) ->
-      hov 1 (str "Change" ++ brk (1,1) ++ pr_constr c ++ pr_clause pr_ident h)
+  | TacChange (occl,c,h) ->
+      hov 1 (str "Change" ++ pr_opt (pr_subterms pr_constr) occl ++ 
+        brk (1,1) ++ pr_constr c ++ pr_clause pr_ident h)
 
   (* Equivalence relations *)
   | (TacReflexivity | TacSymmetry) as x -> pr_atom0 x
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 5a8258cb47..bc8128fd85 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -205,10 +205,13 @@ let rec mlexpr_of_constr = function
   | Topconstr.CMeta (loc,n) -> <:expr< Topconstr.CMeta $dloc$ $mlexpr_of_int n$ >>
   | _ -> failwith "mlexpr_of_constr: TODO"
 
+let mlexpr_of_occ_constr =
+  mlexpr_of_pair (mlexpr_of_list mlexpr_of_int) mlexpr_of_constr
+
 let mlexpr_of_red_expr = function
   | Rawterm.Red b -> <:expr< Rawterm.Red $mlexpr_of_bool b$ >>
   | Rawterm.Hnf -> <:expr< Rawterm.Hnf >>
-  | Rawterm.Simpl -> <:expr< Rawterm.Simpl >>
+  | Rawterm.Simpl o -> <:expr< Rawterm.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >>
   | Rawterm.Cbv f ->
       <:expr< Rawterm.Cbv $mlexpr_of_red_flags f$ >>
   | Rawterm.Lazy f ->
@@ -221,8 +224,7 @@ let mlexpr_of_red_expr = function
   | Rawterm.Fold l ->
       <:expr< Rawterm.Fold $mlexpr_of_list mlexpr_of_constr l$ >>
   | Rawterm.Pattern l ->
-      let f1 = mlexpr_of_list mlexpr_of_int in
-      let f = mlexpr_of_list (mlexpr_of_pair f1 mlexpr_of_constr) in
+      let f = mlexpr_of_list mlexpr_of_occ_constr in
       <:expr< Rawterm.Pattern $f l$ >>
   | Rawterm.ExtraRedExpr (s,c) ->
       let l = mlexpr_of_constr c in
@@ -415,9 +417,10 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacReduce (r,cl) ->
       let l = mlexpr_of_list mlexpr_of_hyp_location cl in
       <:expr< Tacexpr.TacReduce $mlexpr_of_red_expr r$ $l$ >>
-  | Tacexpr.TacChange (c,cl) ->
+  | Tacexpr.TacChange (occl,c,cl) ->
       let l = mlexpr_of_list mlexpr_of_hyp_location cl in
-      <:expr< Tacexpr.TacChange $mlexpr_of_constr c$ $l$ >>
+      let g = mlexpr_of_option mlexpr_of_occ_constr in
+      <:expr< Tacexpr.TacChange $g occl$ $mlexpr_of_constr c$ $l$ >>
 
   (* Equivalence relations *)
   | Tacexpr.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >>