aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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-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
2018-03-04Merge PR #6676: [proofview] goals come with a stateMaxime Dénès
2018-03-04Merge PR #915: Fix rewrite in * side conditionsMaxime Dénès
2018-03-04Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document sup...Maxime Dénès
2018-03-04Remove all uses of Focus in standard library.Théo Zimmermann
2018-03-04Fix typos.Théo Zimmermann
2018-03-03Removing test for bug #2850.Pierre-Marie Pédrot
2018-03-03Adding a test file for evar handling in the VM.Pierre-Marie Pédrot
2018-03-03Handling evars in the VM.Pierre-Marie Pédrot
2018-03-03[compat] Remove "Tactic Pattern Unification"Emilio Jesus Gallego Arias
2018-03-03[compat] Remove "Standard Proposition Elimination"Emilio Jesus Gallego Arias
2018-03-03[compat] Remove "Intuition Iff Unfolding"Emilio Jesus Gallego Arias
2018-03-03[compat] Remove "Injection L2R Pattern Order"Emilio Jesus Gallego Arias
2018-03-02CHANGES entry for #6791.Théo Zimmermann
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
2018-03-02Remove the deprecation for some 8.2-8.5 compatibility aliases.Théo Zimmermann
2018-03-02[VM] Unify Const_sorts and Const_type, and remove Vsort.Maxime Dénès
2018-03-02installer: win: put addons in a separate packageEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 14:20:29 +0000