closed bug 1898: fold x in x; added a reordering primitive tactic

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

1 files changed, 26 insertions, 19 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index da4d95eaa..b4371ac23 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -169,6 +169,8 @@ let internal_cut_rev_replace = internal_cut_rev_gen true
 (* Moving hypotheses *)
 let move_hyp        = Tacmach.move_hyp 
 
+let order_hyps      = Tacmach.order_hyps
+
 (* Renaming hypotheses *)
 let rename_hyp      = Tacmach.rename_hyp
 
@@ -192,25 +194,28 @@ let cofix = function
 
 type tactic_reduction = env -> evar_map -> constr -> constr
 
-(* The following two tactics apply an arbitrary
-   reduction function either to the conclusion or to a 
-   certain hypothesis *)
-
-let reduct_in_concl (redfun,sty) gl = 
-  convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl
-
-let reduct_in_hyp redfun ((_,id),where) gl =
-  let (_,c, ty) = pf_get_hyp gl id in
+let pf_reduce_decl redfun where (id,c,ty) gl =
   let redfun' = pf_reduce redfun gl in
   match c with
   | None -> 
       if where = InHypValueOnly then
 	errorlabstrm "" (pr_id id ++ str "has no value.");
-      convert_hyp_no_check (id,None,redfun' ty) gl
+      (id,None,redfun' ty)
   | Some b ->
       let b' = if where <> InHypTypeOnly then redfun' b else b in
       let ty' =	if where <> InHypValueOnly then redfun' ty else ty in
-      convert_hyp_no_check (id,Some b',ty') gl
+      (id,Some b',ty')
+
+(* The following two tactics apply an arbitrary
+   reduction function either to the conclusion or to a 
+   certain hypothesis *)
+
+let reduct_in_concl (redfun,sty) gl = 
+  convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl
+
+let reduct_in_hyp redfun ((_,id),where) gl =
+  convert_hyp_no_check
+    (pf_reduce_decl redfun where (pf_get_hyp gl id) gl) gl 
 
 let reduct_option redfun = function
   | Some id -> reduct_in_hyp (fst redfun) id 
@@ -238,8 +243,8 @@ let change_on_subterm cv_pb t = function
 let change_in_concl occl t =
   reduct_in_concl ((change_on_subterm Reduction.CUMUL t occl),DEFAULTcast)
 
-let change_in_hyp occl t   =
-  reduct_in_hyp (change_on_subterm Reduction.CONV t occl)
+let change_in_hyp occl t id  =
+  with_check (reduct_in_hyp (change_on_subterm Reduction.CONV t occl) id)
 
 let change_option occl t = function
     Some id -> change_in_hyp occl t id
@@ -276,16 +281,18 @@ let pattern_option l = reduct_option (pattern_occs l,DEFAULTcast)
 (* A function which reduces accordingly to a reduction expression,
    as the command Eval does. *)
 
-let needs_check = function
+let checking_fun = function
   (* Expansion is not necessarily well-typed: e.g. expansion of t into x is
      not well-typed in [H:(P t); x:=t |- G] because x is defined after H *)
-  | Fold _ -> true
-  | _ -> false
+  | Fold _ -> with_check
+  | Pattern _ -> with_check
+  | _ -> (fun x -> x)
 
 let reduce redexp cl goal =
-  (if needs_check redexp then with_check else (fun x -> x))
-    (redin_combinator (Redexpr.reduction_of_red_expr redexp) cl)
-    goal
+  let red = Redexpr.reduction_of_red_expr redexp in
+  match redexp with
+      (Fold _|Pattern _) -> with_check (redin_combinator red cl) goal
+    | _ -> redin_combinator red cl goal
 
 (* Unfolding occurrences of a constant *)