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

2 files changed, 21 insertions, 1 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e3553ddd6d..7fdcded009 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 8c9712e97d..dbb0d7e4f5 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.
+*)