aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
2018-03-06Merge PR #6900: [compat] Remove "Tactic Pattern Unification"Maxime Dénès
2018-03-06Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Maxime Dénès
2018-03-06Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"Maxime Dénès
2018-03-05[coq] Adapt to correct LTAC module packing coq/coq#6869Emilio Jesus Gallego Arias
2018-03-05[toplevel] Modify printing goal strategy.Emilio Jesus Gallego Arias
2018-03-05Fix failing packaging job.Théo Zimmermann
2018-03-05Remove NOPLUGINDOCS optionmrmr1993
2018-03-05Add empty description for @raise statements to satisfy ocamldocmrmr1993
2018-03-05Escape curly braces in ocamldoc commentmrmr1993
2018-03-05Separate vim/emacs fold markers from ocamldoc commentsmrmr1993
2018-03-05Build docs for plugins by default, add NOPLUGINDOCS flag to disablemrmr1993
2018-03-05Change non-documentation comment from ocamldoc stylemrmr1993
2018-03-05Fix formatting of some ocamldoc comments to reduce warningsmrmr1993
2018-03-05Replace invalid tag @raises in ocamldoc comments with @raisemrmr1993
2018-03-05Remove non-existent dependencymrmr1993
2018-03-05Tweak comments to fix ocamldoc errorsmrmr1993
2018-03-05Tidy up ml-doc outut, give it a separate output directorymrmr1993
2018-03-05Use computed deps to generate ml-doc and use implicit mli-doc depsmrmr1993
2018-03-05[build] Simpler byte/opt toplevel build.Emilio Jesus Gallego Arias
2018-03-05CHANGES and tests for with Definition @{univs}Gaëtan Gilbert
2018-03-05Allow universe declarations for [with Definition].Gaëtan Gilbert
2018-03-05Deprecate Focus and Unfocus.Théo Zimmermann
2018-03-05[ssreflect] Export parsing witnesses in mli file.Emilio Jesus Gallego Arias
2018-03-05Sanitize universe declaration in Context (stop using a ref...)Gaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-05configure: -warn-error: now takes a bool so that you can also turn it offEnrico Tassi
2018-03-05configure: profiles (sets of flags)Enrico Tassi
2018-03-05configure: make Prefs a record rather than a module of refsEnrico Tassi
2018-03-05Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadMaxime Dénès
2018-03-04[compat] Remove NOOP and alias deprecated options.Emilio Jesus Gallego Arias
2018-03-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-04ssr: add Prenex Implicits for Some_inj to use it as a viewAnton Trunov
2018-03-04ssr: fix typo in doc commentAnton Trunov
2018-03-04Merge PR #935: Handling evars in the VMMaxime Dénès
2018-03-04ssr: ipats: V82.tactic ~nf_evars:false everywhereEnrico Tassi
2018-03-04Proofview: V82.tactic option to not normalize evarsEnrico Tassi
2018-03-04ssr: rewrite Ssripats and Ssrview in the tactic monadEnrico Tassi
2018-03-04tactics: export e_reduct_in_conclEnrico Tassi
2018-03-04reductionops: remove dead code "bind_assum"Enrico Tassi
2018-03-04proofview: debug API to print a goalEnrico Tassi
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-04Merge PR #6736: [toplevel] Move beautify to its own pass.Maxime Dénès
2018-03-04Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Maxime Dénès
2018-03-04Merge PR #6876: Unify Const_sorts and Const_type, and remove VsortMaxime Dénès
2018-03-04Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...Maxime Dénès
2018-03-04Merge PR #6885: [stm] Partial fix for bug #6884 [location missing from replay...Maxime Dénès
2018-03-04Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872]Maxime Dénès
2018-03-04Merge PR #6882: Harden gitattributes against core.whitespace configuration.Maxime Dénès
2018-03-04Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ...Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 23:51:46 +0000