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 ??).

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

1 files changed, 18 insertions, 0 deletions

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.
+*)