Fix destruct: nf_evar prior to tactic interpretation.

Noticed in CoRN

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17028 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 22 insertions, 3 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index dd05184c4..4bc697a60 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -643,8 +643,8 @@ module V82 = struct
   type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
   let tactic tac =
-    (* spiwack: we ignore the dependencies between goals here, expectingly
-       preserving the semantics of <= 8.2 tactics *)
+    (* spiwack: we ignore the dependencies between goals here,
+       expectingly preserving the semantics of <= 8.2 tactics *)
     (* spiwack: convenience notations, waiting for ocaml 3.12 *)
     let (>>=) = Proof.bind in
     Proof.get >>= fun ps ->
@@ -656,7 +656,7 @@ module V82 = struct
         let g = glsigma.Evd.it in
         ( g, sigma )
       in
-    (* Old style tactics expect the goals normalized with respect to evars. *)
+        (* Old style tactics expect the goals normalized with respect to evars. *)
       let (initgoals,initevd) =
         Goal.list_map Goal.V82.nf_evar ps.comb ps.solution
       in
@@ -666,6 +666,18 @@ module V82 = struct
     with e when catchable_exception e ->
       tclZERO e
 
+
+  (* normalises the evars in the goals, and stores the result in
+     solution. *)
+  let nf_evar_goals =
+    (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+    let (>>=) = Proof.bind in
+    Proof.get >>= fun ps ->
+    let (goals,evd) =
+      Goal.list_map Goal.V82.nf_evar ps.comb ps.solution
+    in
+    Proof.set { ps with solution=evd ; comb=goals }
+
   (* A [Proofview.tactic] version of [Refiner.tclEVARS] *)
   let tclEVARS evd =
     (* spiwack: convenience notations, waiting for ocaml 3.12 *)
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 635f2fd47..adb6ec37d 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -275,6 +275,10 @@ module V82 : sig
   type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma 
   val tactic : tac -> unit tactic
 
+  (* normalises the evars in the goals, and stores the result in
+     solution. *)
+  val nf_evar_goals : unit tactic
+
   val tclEVARS : Evd.evar_map -> unit tactic
 
   val has_unresolved_evar : proofview -> bool
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index eae2be017..4696c2356 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1960,6 +1960,9 @@ and interp_atomic ist tac =
   | TacSimpleInductionDestruct (isrec,h) ->
       h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h)
   | TacInductionDestruct (isrec,ev,(l,el,cls)) ->
+      (* spiwack: some unknown part of destruct needs the goal to be
+         prenormalised. *)
+      Proofview.V82.nf_evar_goals <*>
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let l =