diff options
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 7 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 7 | ||||
| -rw-r--r-- | tactics/tactics.ml | 6 | ||||
| -rw-r--r-- | test-suite/success/intros.v | 17 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Prop.v | 12 |
6 files changed, 32 insertions, 21 deletions
@@ -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) |