diff options
| author | coqbot-app[bot] | 2020-12-15 17:43:59 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-15 17:43:59 +0000 |
| commit | f78f812fcba627a913b8c044626df3642ba17c89 (patch) | |
| tree | 12ff463198be130d49a988f9c9bb1d7349a1d3ed /engine | |
| parent | 46c55ced3d1a78f63b3b50fc12d9760663e87e57 (diff) | |
| parent | cade097ff6e5670b5f4c3ea832b593cf88251fbd (diff) | |
Merge PR #13621: Fast path in tclPROGRESS.
Reviewed-by: herbelin
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/proofview.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 22863f451d..b3061eaa81 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -909,10 +909,11 @@ let tclPROGRESS t = in let test = quick_test || + (CList.same_length initial.comb final.comb && Util.List.for_all2eq begin fun i f -> Progress.goal_equal ~evd:initial.solution ~extended_evd:final.solution (drop_state i) (drop_state f) - end initial.comb final.comb + end initial.comb final.comb) in if not test then tclUNIT res |