aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--CHANGES4
-rw-r--r--doc/refman/RefMan-tac.tex7
-rw-r--r--pretyping/tacred.ml7
-rw-r--r--tactics/tactics.ml6
-rw-r--r--test-suite/success/intros.v17
-rw-r--r--theories/Classes/Morphisms_Prop.v12
6 files changed, 32 insertions, 21 deletions
diff --git a/CHANGES b/CHANGES
index bdd2bdfff..416f0a117 100644
--- a/CHANGES
+++ b/CHANGES
@@ -32,6 +32,10 @@ Tactics
- Tactic notations can now be defined locally to a module (use "Local" prefix).
- Tactic "red" now reduces head beta-iota redexes (potential source of
rare incompatibilities).
+- Tactic "hnf" now reduces inner beta-iota redexes
+ (potential source of rare incompatibilities).
+- Tactic "intro H" now reduces beta-iota redexes if these hide a product
+ (potential source of rare incompatibilities).
Program
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a2d02a4ca..4f4c88d01 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -671,8 +671,8 @@ H}{\it n} or {\tt X}{\it n} is a fresh identifier.
In both cases, the new subgoal is $U$.
If the goal is neither a product nor starting with a let definition,
-the tactic {\tt intro} applies the tactic {\tt red} until the tactic
-{\tt intro} can be applied or the goal is not reducible.
+the tactic {\tt intro} applies the tactic {\tt hnf} until the tactic
+{\tt intro} can be applied or the goal is not head-reducible.
\begin{ErrMsgs}
\item \errindex{No product even after head-reduction}
@@ -2916,7 +2916,8 @@ $\beta\iota\zeta$-reduction rules.
This tactic applies to any goal. It replaces the current goal with its
head normal form according to the $\beta\delta\iota\zeta$-reduction
rules, i.e. it reduces the head of the goal until it becomes a
-product or an irreducible term.
+product or an irreducible term. All inner $\beta\iota$-redexes are also
+reduced.
\Example
The term \verb+forall n:nat, (plus (S n) (S n))+ is not reduced by {\tt hnf}.
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 86195edd2..508569f0d 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -812,7 +812,7 @@ let try_red_product env sigma c =
let red_product env sigma c =
try try_red_product env sigma c
- with Redelimination -> error "Not reducible."
+ with Redelimination -> error "No head constant to reduce."
(*
(* This old version of hnf uses betadeltaiota instead of itself (resp
@@ -882,8 +882,9 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
| CoFix _ | Fix _ -> s'
| _ -> redrec (applist(c, stack)))
| None -> s'
- else s'
- in applist (redrec c)
+ else s' in
+ let simpfun = clos_norm_flags betaiota env sigma in
+ simpfun (applist (redrec c))
let hnf_constr = whd_simpl_orelse_delta_but_fix
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 59e023762..ac783adf3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -443,9 +443,9 @@ let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac gl =
(* that intro do betaiotazeta only when reduction is needed; and *)
(* probably also a pity that intro does zeta *)
try
- tclTHEN try_red_in_concl
- (intro_then_gen loc name_flag move_flag force_flag dep_flag tac) gl
- with Redelimination ->
+ tclTHEN hnf_in_concl
+ (intro_then_gen loc name_flag move_flag false dep_flag tac) gl
+ with RefinerError IntroNeedsProduct ->
user_err_loc(loc,"Intro",str "No product even after head-reduction.")
let intro_gen loc n m f d = intro_then_gen loc n m f d (fun _ -> tclIDTAC)
diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v
index 3599da4dc..25e0ec2f7 100644
--- a/test-suite/success/intros.v
+++ b/test-suite/success/intros.v
@@ -3,5 +3,22 @@
Goal forall A, A -> True.
intros _ _.
+Abort.
+(* This did not work until March 2013, because of underlying "red" *)
+Goal (fun x => True -> True) 0.
+intro H.
+Abort.
+
+(* This should still work, with "intro" calling "hnf" *)
+Goal (fun f => True -> f 0 = f 0) (fun x => x).
+intro H.
+match goal with [ |- 0 = 0 ] => reflexivity end.
+Abort.
+
+(* Somewhat related: This did not work until March 2013 *)
+Goal (fun f => f 0 = f 0) (fun x => x).
+hnf.
+match goal with [ |- 0 = 0 ] => reflexivity end.
+Abort.
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 2252e42fc..6f02ac9f5 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -93,21 +93,9 @@ Program Instance all_iff_morphism {A : Type} :
Program Instance all_impl_morphism {A : Type} :
Proper (pointwise_relation A impl ==> impl) (@all A) | 1.
- Next Obligation.
- Proof.
- unfold pointwise_relation, all in *.
- intuition ; specialize (H x0) ; intuition.
- Qed.
-
Program Instance all_inverse_impl_morphism {A : Type} :
Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@all A) | 1.
- Next Obligation.
- Proof.
- unfold pointwise_relation, all in *.
- intuition ; specialize (H x0) ; intuition.
- Qed.
-
(** Equivalent points are simultaneously accessible or not *)
Instance Acc_pt_morphism {A:Type}(E R : A->A->Prop)