diff options
| -rw-r--r-- | pretyping/reductionops.ml | 4 | ||||
| -rw-r--r-- | test-suite/success/apply.v | 18 |
2 files changed, 21 insertions, 1 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e3553ddd6..7fdcded00 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -517,8 +517,10 @@ let nf_evar sigma = local_strong (whd_evar sigma) (* lazy reduction functions. The infos must be created for each term *) +(* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add + a [nf_evar] here *) let clos_norm_flags flgs env sigma t = - norm_val (create_clos_infos flgs env) (inject ((*nf_evar sigma *)t)) + norm_val (create_clos_infos flgs env) (inject (nf_evar sigma t)) let nf_beta = clos_norm_flags Closure.beta empty_env Evd.empty let nf_betaiota = clos_norm_flags Closure.betaiota empty_env Evd.empty diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 8c9712e97..dbb0d7e4f 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -214,3 +214,21 @@ Lemma eta : forall f : (forall P, P 1), intros. apply H. Qed. + +(* Test propagation of evars from subgoal to brother subgoals *) + + (* This works because unfold calls clos_norm_flags which calls nf_evar *) + +Lemma eapply_evar_unfold : let x:=O in O=x -> 0=O. +intros x H; eapply trans_equal; +[apply H | unfold x;match goal with |- ?x = ?x => reflexivity end]. +Qed. + + (* This does not work (oct 2008) because "match goal" sees "?evar = O" + and not "O = O" + +Lemma eapply_evar : O=O -> 0=O. +intro H; eapply trans_equal; + [apply H | match goal with |- ?x = ?x => reflexivity end]. +Qed. +*) |