Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | | | | | | | | | | * | | | | | | | | | build: win: turn off build/installation of gnu Make | 2018-03-06 | ||
| | | | | | | | | | | * | | | | | | | | | | | Clean-up remove always false useeager argument. | 2018-03-06 | ||
| |_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | ||||
| | | | * | | | | | | | | | | | | | | | | | Remove outdated information regarding the FAQ. | 2018-03-06 | ||
| |_|_|/ / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | * | | | Rename some universe minimizing "normalize" functions to "minimize" | 2018-03-06 | ||
| | | | | | | | | | | | | | | | | * | | | Deprecate UState aliases in Evd. | 2018-03-06 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | Merge PR #6917: Fix failing packaging job. | 2018-03-06 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | * | | | | | | | | | | [compat] Remove "Discriminate Introduction" | 2018-03-06 | ||
| |_|_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | | | | | | | [compat] Remove "Shrink Abstract" | 2018-03-06 | ||
| |_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ... | 2018-03-06 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6795: [ssreflect] Export parsing witnesses in mli file. | 2018-03-06 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | * | | | | | | | | | | ssr: use `apply_type ~typecheck:true` everywhere (fix #6634) | 2018-03-06 | ||
* | | | | | | | | | | | | | | | | | | | | Merge PR #6896: [compat] Remove NOOP deprecated options. | 2018-03-06 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6824: Remove deprecated options related to typeclasses. | 2018-03-06 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6900: [compat] Remove "Tactic Pattern Unification" | 2018-03-06 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6898: [compat] Remove "Intuition Iff Unfolding" | 2018-03-06 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6901: [compat] Remove "Injection L2R Pattern Order" | 2018-03-06 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | * | | | | | | | | | | | | | [toplevel] Modify printing goal strategy. | 2018-03-05 | ||
| |_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | * | | | | | | | | | | | | | | | Fix failing packaging job. | 2018-03-05 | ||
| |_|_|_|_|_|_|/ / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | * | | | | | | | | | | | Remove NOPLUGINDOCS option | 2018-03-05 | ||
| | | | | | | | | | | * | | | | | | | | | | | Add empty description for @raise statements to satisfy ocamldoc | 2018-03-05 | ||
| | | | | | | | | | | * | | | | | | | | | | | Escape curly braces in ocamldoc comment | 2018-03-05 | ||
| | | | | | | | | | | * | | | | | | | | | | | Separate vim/emacs fold markers from ocamldoc comments | 2018-03-05 | ||
| | | | | | | | | | | * | | | | | | | | | | | Build docs for plugins by default, add NOPLUGINDOCS flag to disable | 2018-03-05 | ||
| | | | | | | | | | | * | | | | | | | | | | | Change non-documentation comment from ocamldoc style | 2018-03-05 | ||
| | | | | | | | | | | * | | | | | | | | | | | Fix formatting of some ocamldoc comments to reduce warnings | 2018-03-05 | ||
| | | | | | | | | | | * | | | | | | | | | | | Replace invalid tag @raises in ocamldoc comments with @raise | 2018-03-05 | ||
| | | | | | | | | | | * | | | | | | | | | | | Remove non-existent dependency | 2018-03-05 | ||
| | | | | | | | | | | * | | | | | | | | | | | Tweak comments to fix ocamldoc errors | 2018-03-05 | ||
| | | | | | | | | | | * | | | | | | | | | | | Tidy up ml-doc outut, give it a separate output directory | 2018-03-05 | ||
| | | | | | | | | | | * | | | | | | | | | | | Use computed deps to generate ml-doc and use implicit mli-doc deps | 2018-03-05 | ||
| |_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | * | | | | | | | | | | | | CHANGES and tests for with Definition @{univs} | 2018-03-05 | ||
| | | | | | | | | * | | | | | | | | | | | | Allow universe declarations for [with Definition]. | 2018-03-05 | ||
| | | | | | | | | | | | | | | * | | | | | | Deprecate Focus and Unfocus. | 2018-03-05 | ||
| | | | | | * | | | | | | | | | | | | | | | [ssreflect] Export parsing witnesses in mli file. | 2018-03-05 | ||
| |_|_|_|_|/ / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | | | | | | | Sanitize universe declaration in Context (stop using a ref...) | 2018-03-05 | ||
| | | | | | | |/ / / / / / / / / / / / | ||||
* | | | | | | | | | | | | | | | | | | | Merge PR #6855: Update headers following #6543. | 2018-03-05 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | * | | | | configure: -warn-error: now takes a bool so that you can also turn it off | 2018-03-05 | ||
| | | | | | | | | | | | | | | | * | | | | configure: profiles (sets of flags) | 2018-03-05 | ||
| | | | | | | | | | | | | | | | * | | | | configure: make Prefs a record rather than a module of refs | 2018-03-05 | ||
* | | | | | | | | | | | | | | | | | | | | Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monad | 2018-03-05 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | | | | | | | | | | | | | [compat] Remove NOOP and alias deprecated options. | 2018-03-04 | ||
| | | | | | | | |/ / / / / / / / / / / / | | | | | | | |/| | | | | | | | | | | | | ||||
| | | | | | * / | | | | | | | | | | | | | Remove deprecated options related to typeclasses. | 2018-03-04 | ||
| | | | | | |/ / / / / / / / / / / / / | ||||
| | | | | | | | * | | | | | | | | | | | ssr: add Prenex Implicits for Some_inj to use it as a view | 2018-03-04 | ||
| | | | | | | | * | | | | | | | | | | | ssr: fix typo in doc comment | 2018-03-04 | ||
| | | | | | | |/ / / / / / / / / / / | | | | | | |/| | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | Merge PR #935: Handling evars in the VM | 2018-03-04 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | ||||
| | * | | | | | | | | | | | | | | | | ssr: ipats: V82.tactic ~nf_evars:false everywhere | 2018-03-04 | ||
| | * | | | | | | | | | | | | | | | | Proofview: V82.tactic option to not normalize evars | 2018-03-04 | ||
| | * | | | | | | | | | | | | | | | | ssr: rewrite Ssripats and Ssrview in the tactic monad | 2018-03-04 | ||
| | * | | | | | | | | | | | | | | | | tactics: export e_reduct_in_concl | 2018-03-04 | ||
| | * | | | | | | | | | | | | | | | | reductionops: remove dead code "bind_assum" | 2018-03-04 |