aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-13Merge PR #7477: Support for notations with autonomous only-parsing and ↵Emilio Jesus Gallego Arias
only-printing declarations.
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
It's redundant as a dependency of formal-topology.
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
Not only are most of "forall"s in the manual in Coq notation, but the math notation leads to have a specially long space after the comma.
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
warning have been removed Examples for the use of type classes and canonical structures in automatic proof have been moved to the end.
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
clear_hyps remain with no alternative
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
They are now done on Gitlab CI. The test suite on Windows stays on Appveyor.
2018-05-11Windows packaging build with Gitlab CIMaxime Dénès
We use a specific runner on Inria CloudStack. This allows us to have the same build infrastructure setup for signed and unsigned binary packages. The main Coq repository on Gitlab will produce unsigned binaries, using a runner without secret. On my repository, a one-click operation will sign the packages, making this part of the release process smoother.
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
and canonical structures
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
Currently, `configure.ml` does copy/link some files from `kernel` to `checker` in an ad-hoc way. Instead, it is preferable to add a copy rule to make and let it handle the dependencies properly. This also fixes a dependency bug in Windows, as files wouldn't be properly refreshed if `configure` was not run each time.
2018-05-10finished the example where type class resolution is forcedYves Bertot
2018-05-09[ci] Add mit-plv/cross-cryptoJason Gross
I followed the code for fiat-crypto / fiat-parsers. I hope I didn't miss anything.
2018-05-09This version contains an example of using canonical structures soYves Bertot
that type-checking actually triggers the automatic build of a proof.
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 ↵Théo Zimmermann
and indentation.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-27 09:51:49 +0000