From cad1432683f0fa93efaf64f26803a44f64fd1bd0 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 19 Oct 2008 13:41:20 +0000 Subject: Retour en arrière pour raison de compatibilité sur la suppression du nf_evar dans clos_norm_flags (cf échec dans CoRN.Transc.InvTrigonom.Tan_ilim). Ceci dit : - cela ne me parait pas moral que clos_norm_flags s'occupe de normaliser les evars, - mais comme "evar" n'est pas un flag supporté par closure.ml, on ne peut pas le donner à la demande comme argument de clos_norm_flags (question: pourrait-on faire supporter la réduction Evar par closure.ml ??). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Plus généralement, il y a un problème avec la propagation des instantiations des evars à travers les buts (cf lemme eapply_evar dans test-suite/success/apply.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11470 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/success/apply.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'test-suite/success') 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. +*) -- cgit v1.2.3