aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Merge PR #6905: Fix make ml-docGravatar Maxime Dénès2018-03-07
|\
* \ Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Gravatar Maxime Dénès2018-03-07
|\ \
* \ \ Merge PR #6922: Remove outdated information regarding the FAQ.Gravatar Maxime Dénès2018-03-07
|\ \ \
* \ \ \ Merge PR #6374: [toplevel] Modify printing goal strategy.Gravatar Maxime Dénès2018-03-07
|\ \ \ \
* \ \ \ \ Merge PR #6790: Allow universe declarations for [with Definition].Gravatar Maxime Dénès2018-03-07
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)Gravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \
| | | | * | | Remove outdated information regarding the FAQ.Gravatar Théo Zimmermann2018-03-06
| |_|_|/ / / |/| | | | |
* | | | | | Merge PR #6917: Fix failing packaging job.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6896: [compat] Remove NOOP deprecated options.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6824: Remove deprecated options related to typeclasses.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6900: [compat] Remove "Tactic Pattern Unification"Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | * | | [toplevel] Modify printing goal strategy.Gravatar Emilio Jesus Gallego Arias2018-03-05
| |_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | |
| | | | | | | | * | | | | Fix failing packaging job.Gravatar Théo Zimmermann2018-03-05
| |_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | |
| | | | | | | | | | | * Remove NOPLUGINDOCS optionGravatar mrmr19932018-03-05
| | | | | | | | | | | * Add empty description for @raise statements to satisfy ocamldocGravatar mrmr19932018-03-05
| | | | | | | | | | | * Escape curly braces in ocamldoc commentGravatar mrmr19932018-03-05
| | | | | | | | | | | * Separate vim/emacs fold markers from ocamldoc commentsGravatar mrmr19932018-03-05
| | | | | | | | | | | * Build docs for plugins by default, add NOPLUGINDOCS flag to disableGravatar mrmr19932018-03-05
| | | | | | | | | | | * Change non-documentation comment from ocamldoc styleGravatar mrmr19932018-03-05
| | | | | | | | | | | * Fix formatting of some ocamldoc comments to reduce warningsGravatar mrmr19932018-03-05
| | | | | | | | | | | * Replace invalid tag @raises in ocamldoc comments with @raiseGravatar mrmr19932018-03-05
| | | | | | | | | | | * Remove non-existent dependencyGravatar mrmr19932018-03-05
| | | | | | | | | | | * Tweak comments to fix ocamldoc errorsGravatar mrmr19932018-03-05
| | | | | | | | | | | * Tidy up ml-doc outut, give it a separate output directoryGravatar mrmr19932018-03-05
| | | | | | | | | | | * Use computed deps to generate ml-doc and use implicit mli-doc depsGravatar mrmr19932018-03-05
| |_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | |
| | | | | | | | | * | CHANGES and tests for with Definition @{univs}Gravatar Gaëtan Gilbert2018-03-05
| | | | | | | | | * | Allow universe declarations for [with Definition].Gravatar Gaëtan Gilbert2018-03-05
| | | | | | * | | | | [ssreflect] Export parsing witnesses in mli file.Gravatar Emilio Jesus Gallego Arias2018-03-05
| |_|_|_|_|/ / / / / |/| | | | | | | | |
| | | | | | | * | | Sanitize universe declaration in Context (stop using a ref...)Gravatar Gaëtan Gilbert2018-03-05
| | | | | | | |/ /
* | | | | | | | | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadGravatar Maxime Dénès2018-03-05
|\ \ \ \ \ \ \ \ \ \
| | | | | | | * | | | [compat] Remove NOOP and alias deprecated options.Gravatar Emilio Jesus Gallego Arias2018-03-04
| | | | | | | | |/ / | | | | | | | |/| |
| | | | | | * / | | Remove deprecated options related to typeclasses.Gravatar Théo Zimmermann2018-03-04
| | | | | | |/ / /
| | | | | | | | * ssr: add Prenex Implicits for Some_inj to use it as a viewGravatar Anton Trunov2018-03-04
| | | | | | | | * ssr: fix typo in doc commentGravatar Anton Trunov2018-03-04
| | | | | | | |/ | | | | | | |/|
* | | | | | | | Merge PR #935: Handling evars in the VMGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / |/| | | | | | |
| | * | | | | | ssr: ipats: V82.tactic ~nf_evars:false everywhereGravatar Enrico Tassi2018-03-04
| | * | | | | | Proofview: V82.tactic option to not normalize evarsGravatar Enrico Tassi2018-03-04
| | * | | | | | ssr: rewrite Ssripats and Ssrview in the tactic monadGravatar Enrico Tassi2018-03-04
| | * | | | | | tactics: export e_reduct_in_conclGravatar Enrico Tassi2018-03-04
| | * | | | | | reductionops: remove dead code "bind_assum"Gravatar Enrico Tassi2018-03-04
| | * | | | | | proofview: debug API to print a goalGravatar Enrico Tassi2018-03-04
* | | | | | | | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6736: [toplevel] Move beautify to its own pass.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / |/| | | | | | | |
* | | | | | | | | Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6876: Unify Const_sorts and Const_type, and remove VsortGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ \ \