coq/doc/sphinx/proofs, branch master The formal proof system Remove the omega tactic and related options 2021-04-03T01:52:59+00:00 Jim Fehrle 2021-01-11T22:47:13+00:00 d3a51ac24244f586dfeff1a93b68cb084370534e 






Convert 2nd part of rewriting chapter to prodn
2021-03-08T19:48:20+00:00

Jim Fehrle

2020-09-13T03:54:22+00:00

0d33024ff79c38d52fde49e23d0e45d9c22eefbe












Merge PR #13889: Dead code elimination: not reducible error message is never raised.
2021-03-02T21:27:26+00:00

coqbot-app[bot]

2021-03-02T21:27:26+00:00

a5bea627d1fe742229497b466ca24b470c20d269

Reviewed-by: jfehrle





Reviewed-by: jfehrle







Dead code elimination: not reducible error message is never raised.
2021-03-02T11:27:26+00:00

Théo Zimmermann

2021-03-02T11:27:26+00:00

24fc983730031b53f23bea6fcf2699c73a6dc87d












Infrastructure for fine-grained debug flags
2021-02-24T14:09:15+00:00

Maxime Dénès

2020-10-15T13:31:51+00:00

068031ff7da092c1e2d35db27d713b9606960c42












Update doc/sphinx/proofs/writing-proofs/rewriting.rst
2021-01-28T21:20:07+00:00

Jim Fehrle

2021-01-28T21:20:07+00:00

de7f7fe34828debfa4bd5130810ee5ccc0ea0170












Apply suggestions from code review
2021-01-28T20:18:13+00:00

Théo Zimmermann

2021-01-28T20:18:13+00:00

ae7b304a5a24816d31fbcef1212e15b98bada7a1

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>




Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>






Document how rewrite works regarding occurrence selection.
2021-01-28T12:17:10+00:00

Théo Zimmermann

2021-01-26T11:11:25+00:00

639b75a6a5bc2779c684cb8de0042e287c716590












Merge PR #13754: Improve doc of occurrences and rewrite.
2021-01-22T21:18:09+00:00

coqbot-app[bot]

2021-01-22T21:18:09+00:00

03ce01464a36426f152040c85c9b8cf11b0766fc

Reviewed-by: Zimmi48





Reviewed-by: Zimmi48







Improve doc of occurrences and rewrite.
2021-01-22T20:15:59+00:00

Jim Fehrle

2021-01-08T20:06:24+00:00

e16bbf716b97128272556134b88da2e80c3d115d