coq/doc/sphinx/addendum, branch master The formal proof system Merge PR #13911: Remove the :> type cast? 2021-04-21T14:58:51+00:00 coqbot-app[bot] 2021-04-21T14:58:51+00:00 f9996cdaf0b6aee12c5b71432b1edb90dffb569a Reviewed-by: mattam82 Ack-by: Zimmi48 
Reviewed-by: mattam82
Ack-by: Zimmi48
[zify] bugfix 2021-04-16T21:53:38+00:00 Frederic Besson 2021-04-12T19:02:51+00:00 d2c7022f0e16e6037c0d8c30c837abaad2c8194f - to zify the conclusion, we are using Tactics.apply (not rewrite) Closes #11089 - constrain the arguments of Add Zify X to be GlobRef.t Unset Primitive Projections so that projections are GlobRef.t. Closes #14043 Update doc/sphinx/addendum/micromega.rst Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> 
- to zify the conclusion, we are using Tactics.apply (not rewrite)

Closes #11089

- constrain the arguments of Add Zify X to be GlobRef.t
Unset Primitive Projections so that projections are GlobRef.t.

Closes #14043

Update doc/sphinx/addendum/micromega.rst

Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
Remove the omega tactic and related options 2021-04-03T01:52:59+00:00 Jim Fehrle 2021-01-11T22:47:13+00:00 d3a51ac24244f586dfeff1a93b68cb084370534e 






Remove the :> type cast
2021-03-30T16:51:56+00:00

Jim Fehrle

2021-03-07T18:15:11+00:00

eeb142f3c69d2467fbadd7dd1470ac1606b2e5bf












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 #13781: [micromega] Deprecate hopefully useless options and flags
2021-01-28T20:25:52+00:00

coqbot-app[bot]

2021-01-28T20:25:52+00:00

59dc4eb40e9512d95f73df7a6bc67edcb1907acd

Reviewed-by: Zimmi48
Ack-by: jfehrle





Reviewed-by: Zimmi48
Ack-by: jfehrle







Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)
2021-01-26T11:08:28+00:00

coqbot-app[bot]

2021-01-26T11:08:28+00:00

1a84bed789697ff9b4f5c70dec3c732cdbbdbce0

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48





Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48







Remove the Hide Obligations flag
2021-01-25T18:01:22+00:00

Jim Fehrle

2021-01-19T05:22:52+00:00

7ea0db435910c2db2a9ae4cadfd54f49f3640b62












Update doc/sphinx/addendum/micromega.rst
2021-01-25T09:16:27+00:00

Frédéric Besson

2021-01-25T09:16:27+00:00

b8561224dc91ae7236173022676a907ea93a1ef9

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




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






[micromega] Deprecate hopefully useless options and flags
2021-01-22T21:13:22+00:00

BESSON Frederic

2021-01-22T21:13:22+00:00

641f783cb50c7dd24e23bb44b2fcfb46d0356598

The goal is to eventually only use the Simplex solver and
remove all the code needed for fourier elimination.





The goal is to eventually only use the Simplex solver and
remove all the code needed for fourier elimination.