Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant

fix/cofix avec réutilisation du nom de la constante dans les appels
récursifs), avec notamment uniformisation des comportements et des
noms de fonctions de réduction. En particulier, on a les changements
sémantiques suivants :

- léger changement de simpl: si appliqué à un fix explicite, il sait
  réduire l'argument en un constructeur comme si le fix était caché
  derrière une constante (cf exemple dans test-suite/output/reduction.v);
- léger changement de hnf: si appliqué à un match ou un fix explicite
  et que l'argument de ce match ou de ce fix nécessite un calcul
  impliquant des constantes récursives, il sait conserver les noms (à
  la manière de simpl) comme il sait déjà le faire si ce match ou ce fix
  était caché derrière une constante (cf exemple dans
  test-suite/output/reduction.v);
- changement similaire de one_step_reduce utilisé dans reduce_to_*_ref
  (difficile d'imaginer les effets mais sans doute très peu)



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

9 files changed, 213 insertions, 167 deletions

diff --git a/CHANGES b/CHANGES
index 7a54ecf615..b176fb6856 100644
--- a/CHANGES
+++ b/CHANGES
@@ -26,6 +26,8 @@ Tactics
 
 - New tactics [apply -> term], [apply <- term], [apply -> term in
   ident], [apply <- term in ident] for applying equivalences (iff).
+- Slight improvement of the hnf and simpl tactics when applied on
+  expressions with explicit occurrences of match or fix.
 
 Changes from V8.1gamma to V8.1
 ==============================
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 987d07912f..8c792dc805 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -181,7 +181,8 @@ val is_arity : env ->  evar_map -> constr -> bool
 
 val whd_programs :  reduction_function
 
-(* [reduce_fix] contracts a fix redex if it is actually reducible *)
+(* [reduce_fix redfun fix stk] contracts [fix stk] if it is actually
+   reducible; the structural argument is reduced by [redfun] *)
 
 type fix_reduction_result = NotReducible | Reduced of state
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index d79295c0b1..9c6582bec9 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -90,8 +90,8 @@ let reference_value sigma env c =
     | Some d -> d
 
 (************************************************************************)
-(* Reduction of constant hiding fixpoints (e.g. for Simpl). The trick   *)
-(* is to reuse the name of the function after reduction of the fixpoint *)
+(* Reduction of constants hiding a fixpoint (e.g. for "simpl" tactic).  *)
+(* One reuses the name of the function after reduction of the fixpoint  *)
 
 type constant_evaluation = 
   | EliminationFix of int * (int * (int * constr) list * int)
@@ -103,7 +103,6 @@ type constant_evaluation =
 
 (* We use a cache registered as a global table *)
 
-
 module CstOrdered =
   struct
     type t = constant
@@ -325,20 +324,18 @@ let make_elim_fun (names,(nbfix,lv,n)) largs =
             list_fold_left_i (fun q (* j from comment is n+1-q *) c (ij,tij) ->
               let subst = List.map (lift (-q)) (list_firstn (n-ij) la) in
               let tij' = substl (List.rev subst) tij in
-	      mkLambda (x,tij',c)
-            ) 1 body (List.rev lv)
+	      mkLambda (x,tij',c)) 1 body (List.rev lv)
           in Some g
 
-(* [f] is convertible to [Fix(recindices,bodynum),bodyvect)] make 
-   the reduction using this extra information *)
+(* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]: 
+   do so that the reduction uses this extra information *)
 
 let contract_fix_use_function f
-  ((recindices,bodynum),(types,names,bodies as typedbodies)) =
+  ((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
   let nbodies = Array.length recindices in
   let make_Fi j = match f j with
     | None -> mkFix((recindices,j),typedbodies)
     | Some c -> c in
-(*    match List.nth names j with Name id -> f id | _ -> assert false in*)
   let lbodies = list_tabulate make_Fi nbodies in
   substl (List.rev lbodies) bodies.(bodynum)
 
@@ -358,12 +355,11 @@ let reduce_fix_use_function f whfun fix stack =
 	       Reduced (contract_fix_use_function f fix,stack')
 	   | _ -> NotReducible)
 
-let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) =
+let contract_cofix_use_function f (bodynum,(names,_,bodies as typedbodies)) =
   let nbodies = Array.length bodies in
-  let make_Fi j = match f j with
+  let make_Fi j = match f names.(j) with
     | None -> mkCoFix(j,typedbodies)
     | Some c -> c in
-(*    match List.nth names j with Name id -> f id | _ -> assert false in*)
   let subbodies = list_tabulate make_Fi nbodies in
   substl subbodies bodies.(bodynum)
 
@@ -372,19 +368,16 @@ let reduce_mind_case_use_function func env mia =
     | Construct(ind_sp,i) ->
 	let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in
 	applist (mia.mlf.(i-1), real_cargs)
-    | CoFix (_,(names,_,_) as cofix) ->
-	let build_fix_name i =
-	  match names.(i) with 
-	    | Name id ->
-                if isConst func then
-		  let (mp,dp,_) = repr_con (destConst func) in
-		  let kn = make_con mp dp (label_of_id id) in
-		  (match constant_opt_value env kn with
-		    | None -> None
-		    | Some _ -> Some (mkConst kn))
-                else None
-	    | Anonymous -> None in 
-	let cofix_def = contract_cofix_use_function build_fix_name cofix in
+    | CoFix cofix ->
+	let build_cofix_name = function
+	  | Name id when isConst func ->
+	      let (mp,dp,_) = repr_con (destConst func) in
+	      let kn = make_con mp dp (label_of_id id) in
+	      (match constant_opt_value env kn with
+		| None -> None
+		| Some _ -> Some (mkConst kn))
+	  | _ -> None in 
+	let cofix_def = contract_cofix_use_function build_cofix_name cofix in
 	mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 
@@ -412,20 +405,23 @@ let special_red_case sigma env whfun (ci, p, c, lf)  =
   in 
   redrec (c, empty_stack)
 
+(* [red_elim_const] contracts iota/fix/cofix redexes hidden behind
+   constants by keeping the name of the constants in the recursive calls;
+   it fails if no redex is around *)
 
 let rec red_elim_const env sigma ref largs =
   match reference_eval sigma env ref with
     | EliminationCases n when stack_args_size largs >= n ->
 	let c = reference_value sigma env ref in
 	let c', lrest = whd_betadelta_state env sigma (c,largs) in
-        (special_red_case sigma env (construct_const env sigma) (destCase c'),
-	 lrest)
+	let whfun = whd_simpl_state env sigma in
+        (special_red_case sigma env whfun (destCase c'), lrest)
     | EliminationFix (min,infos) when stack_args_size largs >=min ->
 	let c = reference_value sigma env ref in
 	let d, lrest = whd_betadelta_state env sigma (c,largs) in
 	let f = make_elim_fun ([|Some ref|],infos) largs in
-	let co = construct_const env sigma in
-	(match reduce_fix_use_function f co (destFix d) lrest with
+	let whfun = whd_construct_state env sigma in
+	(match reduce_fix_use_function f whfun (destFix d) lrest with
 	   | NotReducible -> raise Redelimination
 	   | Reduced (c,rest) -> (nf_beta c, rest))
     | EliminationMutualFix (min,refgoal,refinfos)
@@ -440,53 +436,65 @@ let rec red_elim_const env sigma ref largs =
 	let (_, midargs as s) = descend ref largs in
 	let d, lrest = whd_betadelta_state env sigma s in
 	let f = make_elim_fun refinfos midargs in
-	let co = construct_const env sigma in
-	(match reduce_fix_use_function f co (destFix d) lrest with
+	let whfun = whd_construct_state env sigma in
+	(match reduce_fix_use_function f whfun (destFix d) lrest with
 	   | NotReducible -> raise Redelimination
 	   | Reduced (c,rest) -> (nf_beta c, rest))
     | _ -> raise Redelimination
 
-and construct_const env sigma = 
-  let rec hnfstack (x, stack as s) =
+(* reduce to whd normal form or to an applied constant that does not hide
+   a reducible iota/fix/cofix redex (the "simpl" tactic) *)
+
+and whd_simpl_state env sigma s =
+  let rec redrec (x, stack as s) =
     match kind_of_term x with
-      | Cast (c,_,_) -> hnfstack (c, stack)
-      | App (f,cl) -> hnfstack (f, append_stack cl stack)
-      | Lambda (id,t,c) ->
+      | Lambda (na,t,c) ->
           (match decomp_stack stack with 
-             | None -> assert false
-             | Some (c',rest) -> 
-		   stacklam hnfstack [c'] c rest)
-      | LetIn (n,b,t,c) -> stacklam hnfstack [b] c stack
+             | None -> s
+             | Some (a,rest) -> stacklam redrec [a] c rest)
+      | LetIn (n,b,t,c) -> stacklam redrec [b] c stack
+      | App (f,cl) -> redrec (f, append_stack cl stack)
+      | Cast (c,_,_) -> redrec (c, stack)
       | Case (ci,p,c,lf) ->
-          hnfstack 
-	    (special_red_case sigma env
-              (construct_const env sigma) (ci,p,c,lf), stack)
-      | Construct _ -> s
-      | CoFix _ -> s
-      | Fix fix -> 
-	  (match reduce_fix hnfstack fix stack with
-             | Reduced s' -> hnfstack s'
-	     | NotReducible -> raise Redelimination)
+          (try 
+	    redrec (special_red_case sigma env redrec (ci,p,c,lf), stack)
+	  with
+	      Redelimination -> s)
+      | Fix fix ->
+	  (try match reduce_fix (whd_construct_state env sigma) fix stack with
+            | Reduced s' -> redrec s'
+	    | NotReducible -> s
+	  with Redelimination -> s)
       | _ when isEvalRef env x ->
 	  let ref = destEvalRef x in
           (try
-	    hnfstack (red_elim_const env sigma ref stack)
+	    redrec (red_elim_const env sigma ref stack)
            with Redelimination ->
-	     (match reference_opt_value sigma env ref with
-		| Some cval ->
-		    (match kind_of_term cval with
-                       | CoFix _ -> s
-                       | _ -> hnfstack (cval, stack))
-		| None ->
-		    raise Redelimination))
-      | _ -> raise Redelimination
+	     s)
+      | _ -> s
   in 
-  hnfstack 
+  redrec s
+
+(* reduce until finding an applied constructor or fail *)
+
+and whd_construct_state env sigma s =
+  let (constr, cargs as s') = whd_simpl_state env sigma s in 
+  if reducible_mind_case constr then s'
+  else if isEvalRef env constr then
+    let ref = destEvalRef constr in
+    match reference_opt_value sigma env ref with
+      | None -> raise Redelimination
+      | Some gvalue -> whd_construct_state env sigma (gvalue, cargs)
+  else
+    raise Redelimination
 
 (************************************************************************)
 (*            Special Purpose Reduction Strategies                     *)
 
-(* Red reduction tactic: reduction to a product *)
+(* Red reduction tactic: one step of delta reduction + full
+   beta-iota-fix-cofix-zeta-cast at the head of the conclusion of a
+   sequence of products; fails if no delta redex is around
+*)
 
 let try_red_product env sigma c = 
   let simpfun = clos_norm_flags betaiotazeta env sigma in
@@ -521,77 +529,89 @@ let red_product env sigma c =
   try try_red_product env sigma c
   with Redelimination -> error "Not reducible"
 
-let hnf_constr env sigma c = 
-  let rec redrec (x, largs as s) =
+(*
+(* This old version of hnf uses betadeltaiota instead of itself (resp 
+   whd_construct_state) to reduce the argument of Case (resp Fix);
+   The new version uses the "simpl" strategy instead. For instance,
+
+   Variable n:nat.
+   Eval hnf in match (plus (S n) O) with S n => n | _ => O end.  
+
+   returned
+
+   (fix plus (n m : nat) {struct n} : nat :=
+        match n with
+        | O => m
+        | S p => S (plus p m)
+        end) n 0
+
+   while the new version returns (plus n O)
+ *)
+
+let whd_simpl_orelse_delta_but_fix_old env sigma c =
+  let whd_all = whd_betadeltaiota_state env sigma in
+  let rec redrec (x, stack as s) =
     match kind_of_term x with
-      | Lambda (n,t,c) ->
-          (match decomp_stack largs with
-             | None      -> app_stack s
-             | Some (a,rest) -> 
-		 stacklam redrec [a] c rest)
-      | LetIn (n,b,t,c) -> stacklam redrec [b] c largs
-      | App (f,cl)   -> redrec (f, append_stack cl largs)
-      | Cast (c,_,_) -> redrec (c, largs)
-      | Case (ci,p,c,lf) ->
+      | Lambda (na,t,c) ->
+          (match decomp_stack stack with
+             | None      -> s
+             | Some (a,rest) -> stacklam redrec [a] c rest)
+      | LetIn (n,b,t,c) -> stacklam redrec [b] c stack
+      | App (f,cl)   -> redrec (f, append_stack cl stack)
+      | Cast (c,_,_) -> redrec (c, stack)
+      | Case (ci,p,d,lf) ->
           (try
-             redrec 
-	       (special_red_case sigma env (whd_betadeltaiota_state env sigma) 
-		  (ci, p, c, lf), largs)
+             redrec (special_red_case sigma env whd_all (ci,p,d,lf), stack)
            with Redelimination -> 
-	     app_stack s)
+	     s)
       | Fix fix ->
-	  (match reduce_fix (whd_betadeltaiota_state env sigma) fix largs with
+	  (match reduce_fix whd_all fix stack with
              | Reduced s' -> redrec s'
-	     | NotReducible -> app_stack s)
+	     | NotReducible -> s)
       | _ when isEvalRef env x ->
 	  let ref = destEvalRef x in
           (try
-            let (c',lrest) = red_elim_const env sigma ref largs in 
-	    redrec (c', lrest)
+	    redrec (red_elim_const env sigma ref stack)
            with Redelimination ->
              match reference_opt_value sigma env ref with
 	       | Some c ->
 		   (match kind_of_term (snd (decompose_lam c)) with 
-                      | CoFix _ | Fix _ -> app_stack (x,largs)
-		      | _ -> redrec (c, largs))
-	       | None -> app_stack s)
-      | _ -> app_stack s
-  in 
-  redrec (c, empty_stack)
+                     | CoFix _ | Fix _ -> s
+		     | _ -> redrec (c, stack))
+	       | None -> s)
+      | _ -> s
+  in app_stack (redrec (c, empty_stack))
+*)
 
-(* Simpl reduction tactic: same as simplify, but also reduces
-   elimination constants *)
+(* Same as [whd_simpl] but also reduces constants that do not hide a
+   reducible fix, but does this reduction of constants only until it
+   it immediately hides a non reducible fix or a cofix *)
 
-let whd_nf env sigma c = 
-  let rec nf_app (c, stack as s) =
-    match kind_of_term c with
-      | Lambda (name,c1,c2)    ->
-          (match decomp_stack stack with
-             | None -> (c,empty_stack)
-             | Some (a1,rest) -> 
-		 stacklam nf_app [a1] c2 rest)
-      | LetIn (n,b,t,c) -> stacklam nf_app [b] c stack
-      | App (f,cl) -> nf_app (f, append_stack cl stack)
-      | Cast (c,_,_) -> nf_app (c, stack)
-      | Case (ci,p,d,lf) ->
-          (try
-             nf_app (special_red_case sigma env nf_app (ci,p,d,lf), stack)
-           with Redelimination -> 
-	     s)
-      | Fix fix ->
-	  (match reduce_fix nf_app fix stack with
-             | Reduced s' -> nf_app s'
-	     | NotReducible -> s)
-      | _ when isEvalRef env c ->
-          (try
-	     nf_app (red_elim_const env sigma (destEvalRef c) stack)
-           with Redelimination -> 
-	     s)
-      | _ -> s
-  in 
-  app_stack (nf_app (c, empty_stack))
+let whd_simpl_orelse_delta_but_fix env sigma c =
+  let rec redrec s =
+    let (constr, stack as s') = whd_simpl_state env sigma s in 
+    if isEvalRef env constr then
+      match reference_opt_value sigma env (destEvalRef constr) with
+	| Some c ->
+	    (match kind_of_term (snd (decompose_lam c)) with 
+              | CoFix _ | Fix _ -> s'
+	      | _ -> redrec (c, stack))
+	| None -> s'
+    else s'
+  in app_stack (redrec (c, empty_stack))
+
+let hnf_constr = whd_simpl_orelse_delta_but_fix
+
+(* The "simpl" reduction tactic *)
+
+let whd_simpl env sigma c =
+  app_stack (whd_simpl_state env sigma (c, empty_stack))
+
+let simpl env sigma c = strong whd_simpl env sigma c
 
-let nf env sigma c = strong whd_nf env sigma c
+let nf = simpl (* Compatibility *)
+
+(* Reduction at specific subterms *)
 
 let is_head c t =
   match kind_of_term t with
@@ -808,69 +828,66 @@ let pattern_occs loccs_trm env sigma c =
 
 (* Used in several tactics. *)
 
+(* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name
+   return name, B and t' *)
+
+let reduce_to_ind_gen allow_product env sigma t = 
+  let rec elimrec env t l =
+    let t = hnf_constr env sigma t in
+    match kind_of_term (fst (decompose_app t)) with
+      | Ind ind-> (ind, it_mkProd_or_LetIn t l)
+      | Prod (n,ty,t') ->
+	  if allow_product then
+	    elimrec (push_rel (n,None,ty) env) t' ((n,None,ty)::l)
+	  else
+	     errorlabstrm "tactics__reduce_to_mind"
+	       (str"Not an inductive definition")
+      | _ ->
+	  errorlabstrm "tactics__reduce_to_mind"
+	    (str"Not an inductive product")
+  in
+  elimrec env t []
+
+let reduce_to_quantified_ind x = reduce_to_ind_gen true x
+let reduce_to_atomic_ind x = reduce_to_ind_gen false x
+
+(* Reduce the weak-head redex [beta,iota/fix/cofix[all],cast,zeta,simpl/delta]
+   or raise [NotStepReducible] if not a weak-head redex *)
+
 exception NotStepReducible
 
 let one_step_reduce env sigma c = 
-  let rec redrec (x, largs) =
+  let rec redrec (x, stack) =
     match kind_of_term x with
       | Lambda (n,t,c)  ->
-          (match decomp_stack largs with
+          (match decomp_stack stack with
              | None      -> raise NotStepReducible
              | Some (a,rest) -> (subst1 a c, rest))
-      | App (f,cl) -> redrec (f, append_stack cl largs)
-      | LetIn (_,f,_,cl) -> (subst1 f cl,largs)
+      | App (f,cl) -> redrec (f, append_stack cl stack)
+      | LetIn (_,f,_,cl) -> (subst1 f cl,stack)
+      | Cast (c,_,_) -> redrec (c,stack)
       | Case (ci,p,c,lf) ->
           (try
-	     (special_red_case sigma env (whd_betadeltaiota_state env sigma)
-	       (ci,p,c,lf), largs)
+	     (special_red_case sigma env (whd_simpl_state env sigma)
+	       (ci,p,c,lf), stack)
            with Redelimination -> raise NotStepReducible)
       | Fix fix ->
-	  (match reduce_fix (whd_betadeltaiota_state env sigma) fix largs with
+	  (match reduce_fix (whd_construct_state env sigma) fix stack with
              | Reduced s' -> s'
 	     | NotReducible -> raise NotStepReducible)
-      | Cast (c,_,_) -> redrec (c,largs)
       | _ when isEvalRef env x ->
-	  let ref =
-            try destEvalRef x
-            with Redelimination -> raise NotStepReducible in
+	  let ref = destEvalRef x in
           (try
-            red_elim_const env sigma ref largs
+            red_elim_const env sigma ref stack
            with Redelimination ->
 	     match reference_opt_value sigma env ref with
-	       | Some d -> d, largs
+	       | Some d -> d, stack
 	       | None -> raise NotStepReducible)
 
       | _ -> raise NotStepReducible
   in 
   app_stack (redrec (c, empty_stack))
 
-(* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name
-   return name, B and t' *)
-
-let reduce_to_ind_gen allow_product env sigma t = 
-  let rec elimrec env t l = 
-    let c, _ = Reductionops.whd_stack t in
-    match kind_of_term c with
-      | Ind (mind,args) -> ((mind,args),it_mkProd_or_LetIn t l)
-      | Prod (n,ty,t') ->
-	  if allow_product then
-	    elimrec (push_rel (n,None,t) env) t' ((n,None,ty)::l)
-	  else
-	     errorlabstrm "tactics__reduce_to_mind"
-	       (str"Not an inductive definition")
-      | _ ->
-          (try 
-	     let t' = nf_betaiota (one_step_reduce env sigma t) in 
-	     elimrec env t' l
-           with NotStepReducible ->
-	     errorlabstrm "tactics__reduce_to_mind"
-               (str"Not an inductive product"))
-  in
-  elimrec env t []
-
-let reduce_to_quantified_ind x = reduce_to_ind_gen true x
-let reduce_to_atomic_ind x = reduce_to_ind_gen false x
-
 let reduce_to_ref_gen allow_product env sigma ref t = 
   let rec elimrec env t l = 
     let c, _ = Reductionops.whd_stack t in
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 84cc87e7f0..0ff5154f60 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -35,11 +35,15 @@ val red_product : reduction_function
 (* Red (raise Redelimination if nothing reducible) *)
 val try_red_product : reduction_function
 
-(* Hnf *)
-val hnf_constr :  reduction_function
-
 (* Simpl *)
-val nf :  reduction_function
+val simpl : reduction_function 
+
+(* Simpl only at the head *)
+val whd_simpl : reduction_function
+
+(* Hnf: like whd_simpl but force delta-reduction of constants that do
+   not immediately hide a non reducible fix or cofix *)
+val hnf_constr : reduction_function
 
 (* Unfold *)
 val unfoldn : 
@@ -79,3 +83,8 @@ val reduce_to_atomic_ref :
 
 val contextually : bool -> int list * constr -> reduction_function
   -> reduction_function
+
+(* Compatibility *)
+(* use [simpl] instead of [nf] *)
+val nf :  reduction_function
+
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index c69d1be364..2f85b18e58 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -106,8 +106,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) nf,DEFAULTcast)
-  | Simpl None -> (nf,DEFAULTcast)
+    (contextually (is_reference c) (out_with_occurrences lp) simpl,DEFAULTcast)
+  | Simpl None -> (simpl,DEFAULTcast)
   | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast)
   | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast)
   | Unfold ubinds -> (unfoldn (List.map out_with_occurrences ubinds),DEFAULTcast)
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 500a7f40d3..1273c65e45 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -903,7 +903,7 @@ let new_morphism m signature id hook =
       (Closure.unfold_red(Lazy.force coq_make_compatibility_goal_aux_eval_ref))
       env Evd.empty lem in
     (* "simpl" *)
-  let lem = Tacred.nf env Evd.empty lem in
+  let lem = Tacred.simpl env Evd.empty lem in
     if Lib.is_modtype () then
       begin
 	ignore
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9e25055e9c..f9e623469e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -208,9 +208,9 @@ let red_option          = reduct_option   (red_product,DEFAULTcast)
 let hnf_in_concl        = reduct_in_concl (hnf_constr,DEFAULTcast)
 let hnf_in_hyp          = reduct_in_hyp   hnf_constr
 let hnf_option          = reduct_option   (hnf_constr,DEFAULTcast)
-let simpl_in_concl      = reduct_in_concl (nf,DEFAULTcast)
-let simpl_in_hyp        = reduct_in_hyp   nf
-let simpl_option        = reduct_option   (nf,DEFAULTcast)
+let simpl_in_concl      = reduct_in_concl (simpl,DEFAULTcast)
+let simpl_in_hyp        = reduct_in_hyp   simpl
+let simpl_option        = reduct_option   (simpl,DEFAULTcast)
 let normalise_in_concl  = reduct_in_concl (compute,DEFAULTcast)
 let normalise_in_hyp    = reduct_in_hyp   compute
 let normalise_option    = reduct_option   (compute,DEFAULTcast)
diff --git a/test-suite/output/reduction.out b/test-suite/output/reduction.out
new file mode 100644
index 0000000000..ff327aa5f1
--- /dev/null
+++ b/test-suite/output/reduction.out
@@ -0,0 +1,4 @@
+     = a
+     : nat
+     = n + 0
+     : nat
diff --git a/test-suite/output/reduction.v b/test-suite/output/reduction.v
new file mode 100644
index 0000000000..4a460a83fa
--- /dev/null
+++ b/test-suite/output/reduction.v
@@ -0,0 +1,13 @@
+(* Test the behaviour of hnf and simpl introduced in revision *)
+
+Variable n:nat.
+Definition a:=0.
+
+Eval simpl in (fix plus (n m : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S p => S (p + m)
+  end) a a.
+
+Eval hnf in match (plus (S n) O) with S n => n | _ => O end.  
+