diff options
| author | Arnaud Spiwack | 2014-10-16 15:13:58 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-16 15:14:20 +0200 |
| commit | b5c5f67c628e6ba7c987e9a306f7a0efdebf85cf (patch) | |
| tree | c5329f5848a7020f457735a3c793ce7f00f9c0f1 | |
| parent | 55b626fadb1bffb27cfd4069e2933db0e4784409 (diff) | |
Grab Existential Variables: restore the goal order from v8.4.
Changes in the implementation details had unwittingly changed the order in which Grab Existential Variables displayed the goals.
| -rw-r--r-- | proofs/proofview.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index d387bbf597..dd15159181 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -872,7 +872,7 @@ module V82 = struct (* Main function in the implementation of Grab Existential Variables.*) let grab pv = let undef = Evd.undefined_map pv.solution in - let goals = List.map fst (Evar.Map.bindings undef) in + let goals = List.rev_map fst (Evar.Map.bindings undef) in { pv with comb = goals } |