aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-05-13Merge PR #7477: Support for notations with autonomous only-parsing and only-p...Emilio Jesus Gallego Arias
2018-05-13Merge PR #7489: gitlab CI: remove math-classes jobEmilio Jesus Gallego Arias
2018-05-13Fix #4403: insufficient handling of type-in-type in kernel.Gaëtan Gilbert
2018-05-12adds a hello world tactic in tuto0Yves Bertot
2018-05-12Sphinx: a "QUICK=1" option to bypass recompilation of the library.Hugo Herbelin
2018-05-11gitlab CI: remove math-classes jobGaëtan Gilbert
2018-05-11Merge PR #7340: Remove DirClosedSection.Enrico Tassi
2018-05-11Doc: Renaming an old-style numerical evar in an alphabetical one.Hugo Herbelin
2018-05-11Doc: Moving `\forall` to `forall` in file tactics.rst.Hugo Herbelin
2018-05-11Doc: Some quotes missing in file tactics.rst.Hugo Herbelin
2018-05-11Replacing a broken reference by hyperlinks in chapter tactics.Hugo Herbelin
2018-05-11A few fixes in chapter tactics.Hugo Herbelin
2018-05-11Merge PR #7470: use at least 6 Xs in mktemp filename templatesGaëtan Gilbert
2018-05-11Updates the contents of the third tutorialYves Bertot
2018-05-11This version contains documentation for the code of the packing tacticYves Bertot
2018-05-11Merge PR #6959: [build] Build checker generated files using a make rule.Enrico Tassi
2018-05-11Update old parts of CHANGES to use current bug numbers.Théo Zimmermann
2018-05-11Fix non-portable shebang in test-suite.Théo Zimmermann
2018-05-11Notations: advertize that distinct "only parsing"/"only printing" rules work.Hugo Herbelin
2018-05-11Merge PR #7466: Remove tutorials from the repoMaxime Dénès
2018-05-11Merge PR #7461: [sphinx] Improve the proof handling chapter.Maxime Dénès
2018-05-11Merge PR #7341: Don't recurse into closed modules/sections in split_lib.Enrico Tassi
2018-05-11coqdev.el: add bug-reference-mode variablesGaëtan Gilbert
2018-05-11set_solve_evars doesn't use an evar_map refGaëtan Gilbert
2018-05-11Deprecate Evarconv.e_conv,e_cumulGaëtan Gilbert
2018-05-11Convert clear_hyps_in_evi to state passing style.Gaëtan Gilbert
2018-05-11Deprecate most evarutil evdref functionsGaëtan Gilbert
2018-05-11Merge PR #7363: [ci] Fix another issue with the timing testsGaëtan Gilbert
2018-05-11Adds a tactic that hides the contents of an hypothesis from viewYves Bertot
2018-05-11Use the more colloquial EConstr.t type instead of EConstr.constrYves Bertot
2018-05-11Merge PR #7456: [toplevel] Don't ignore output filename provided by user in -oThéo Zimmermann
2018-05-11Remove packaging jobs from appveyorMaxime Dénès
2018-05-11Windows packaging build with Gitlab CIMaxime Dénès
2018-05-10Merge PR #7437: [coqdep] Minor cleanups.Pierre-Marie Pédrot
2018-05-10Suggest going to /documentation to see a list of tutorials.Théo Zimmermann
2018-05-10One can build all the HTML doc using default.nix.Théo Zimmermann
2018-05-10Clean-up in Makefile.doc and include Sphinx in doc-html target.Théo Zimmermann
2018-05-10Remove tutorials.Théo Zimmermann
2018-05-10Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Hugo Herbelin
2018-05-10Fixes part 1 of #7462 (only-printing not to override existing interp rule).Hugo Herbelin
2018-05-10Merge PR #7473: [ci] Add mit-plv/cross-cryptoEmilio Jesus Gallego Arias
2018-05-10This version has type inference performing proofs, using both type classesYves Bertot
2018-05-10Merge PR #7471: [travis] Fix version of camlp5 for OCaml 4.06.1.Emilio Jesus Gallego Arias
2018-05-10[build] Build checker generated files using a make rule.Emilio Jesus Gallego Arias
2018-05-10finished the example where type class resolution is forcedYves Bertot
2018-05-09[ci] Add mit-plv/cross-cryptoJason Gross
2018-05-09This version contains an example of using canonical structures soYves Bertot
2018-05-09[sphinx] Improve proof handling chapter.Théo Zimmermann
2018-05-09Clarify that the description of coqtop does not reflect all user interfaces.Théo Zimmermann
2018-05-09[sphinx] Improvements around the Show commands, including missing indices and...Théo Zimmermann