diff options
| author | Emilio Jesus Gallego Arias | 2019-04-02 12:15:58 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-02 12:15:58 +0200 |
| commit | 32dbd76a5df76491e029583abf247524f8d26c44 (patch) | |
| tree | 25185fd3ad82c6c5e2e39ed35c0c2eccf5064ea1 /engine/proofview.ml | |
| parent | 424c1973e96dfbf3b2e3245d735853ffa9600373 (diff) | |
| parent | bf840bafc19deba67e5270dfd31b8b6662b73132 (diff) | |
Merge PR #9659: Fix #9652: rewrite fails to detect lack of progress
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Reviewed-by: ppedrot
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 2d693e0259..316f02bc37 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -899,8 +899,8 @@ module Progress = struct (** Equality function on goals *) let goal_equal evars1 gl1 evars2 gl2 = - let evi1 = Evd.find evars1 (drop_state gl1) in - let evi2 = Evd.find evars2 (drop_state gl2) in + let evi1 = Evd.find evars1 gl1 in + let evi2 = Evd.find evars2 gl2 in eq_evar_info evars1 evars2 evi1 evi2 end @@ -918,7 +918,7 @@ let tclPROGRESS t = let test = quick_test || Util.List.for_all2eq begin fun i f -> - Progress.goal_equal initial.solution i final.solution f + Progress.goal_equal initial.solution (drop_state i) final.solution (drop_state f) end initial.comb final.comb in if not test then |