aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* document the Fail commandGravatar Paul Steckler2018-01-25
|
* Merge PR #6551: Bracket with goal selectorGravatar Maxime Dénès2018-01-16
|\
* \ Merge PR #6489: Update PNGs; mention async error handling; change query ↵Gravatar Maxime Dénès2018-01-08
|\ \ | | | | | | | | | window to query pane in text
* \ \ Merge PR #6497: Add optimize_heap tactic for #6488Gravatar Maxime Dénès2018-01-08
|\ \ \
* \ \ \ Merge PR #6526: Fixing various typos in the Credits chapter.Gravatar Maxime Dénès2018-01-08
|\ \ \ \
| | | | * Documentation and CHANGES for bracket with goal selector.Gravatar Théo Zimmermann2018-01-05
| |_|_|/ |/| | |
| | * | add optimize_heap tactic for #6488Gravatar Paul Steckler2018-01-03
| |/ / |/| |
| | * update PNGs; mention async error handling; change query window to query ↵Gravatar Paul Steckler2018-01-03
| |/ |/| | | | | pane; use color descriptions
* | Merge PR #6377: Removal of the FAQ LaTex document.Gravatar Maxime Dénès2017-12-20
|\ \
* | | Fix typo in the refman.Gravatar Théo Zimmermann2017-12-19
| | |
* | | Merge PR #6381: A version of [time] that works on constr evaluationGravatar Maxime Dénès2017-12-18
|\ \ \
* \ \ \ Merge PR #6380: Add tactics to reset and display the Ltac profileGravatar Maxime Dénès2017-12-18
|\ \ \ \
* \ \ \ \ Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵Gravatar Maxime Dénès2017-12-18
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | Extraction Language command
| | | | * | Removing the FAQ, which has been moved to the GitHub wiki for thisGravatar Matt Quinn2017-12-18
| | | | | | | | | | | | | | | | | | | | | | | | repository. Also removing FAQ-related build rules.
* | | | | | [doc] Nit on the manual.Gravatar Emilio Jesus Gallego Arias2017-12-17
| | | | | | | | | | | | | | | | | | | | | | | | `ssrnat` is mentioned, but it is not distributed with Coq.
* | | | | | Merge PR #6219: Document undocumented optionsGravatar Maxime Dénès2017-12-15
|\ \ \ \ \ \
| | | | * | | Add documentation for time_constrGravatar Jason Gross2017-12-14
| | | |/ / /
| | | * / / Add doc+changelog entries for new LtacProf tacticsGravatar Jason Gross2017-12-14
| |_|/ / / |/| | | |
* | | | | Merge PR #978: In printing, experimenting factorizing "match" clauses with ↵Gravatar Maxime Dénès2017-12-14
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | same right-hand side.
* \ \ \ \ \ Merge PR #6169: Clean up/deprecated optionsGravatar Maxime Dénès2017-12-14
|\ \ \ \ \ \
| | | * | | | Document Short Module Printing.Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Document Rewriting Schemes (quickly).Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Document Record Elimination Schemes.Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Document Asymmetric Patterns.Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Document some omega options (missing Omega Oldstyle).Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Add doc for Set Debug RAKAM.Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Add doc for Set Debug Cbv.Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Add doc for Set Info/Debug Auto/Trivial/Eauto.Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Add optindex for Set Bullet Behavior.Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Add doc for Set Congruence VerboseGravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | | * | | | Fix typo in doc optindex for Typeclass Resolution ...Gravatar Gaëtan Gilbert2017-12-14
| | | | | | |
| | * | | | | Documenting the new options for printing "match".Gravatar Hugo Herbelin2017-12-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Namely: - Set Printing Factorizable Match Patterns. = Set Printing Allow Default Clause.
| * | | | | | Remove deprecated appcontext and corresponding documentation.Gravatar Théo Zimmermann2017-12-11
| |/ / / / /
* | | | | | [make] remove unneeded generated file "tolink.ml"Gravatar Emilio Jesus Gallego Arias2017-12-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When statically linking plugins, the "DECLARE PLUGIN" macro takes care of properly setting up the loaded module table. This setup was also done by `coqmktop`, thus in order to ease bisecting, we didn't take care of it in the `coqmktop` deprecation. Fixes #6364.
* | | | | | [build] Remove coqmktop in favor of ocamlfind.Gravatar Emilio Jesus Gallego Arias2017-12-10
|/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind.
* | | | | Merge PR #6277: Qualified import in coqchkGravatar Maxime Dénès2017-12-07
|\ \ \ \ \
| | | * | | use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguageGravatar Paul Steckler2017-12-05
| |_|/ / / |/| | | |
* | | | | Merge PR #890: Global universe declarationsGravatar Maxime Dénès2017-12-05
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6300: Clarify operation of sequences, fixes #6095Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212Gravatar Maxime Dénès2017-12-05
|\ \ \ \ \ \ \ | |_|_|_|_|/ / |/| | | | | |
| | * | | | | clarify operation of sequences, #6095Gravatar Paul Steckler2017-12-01
| | | | | | |
| | | * | | | [refman] Expand a little on global universes.Gravatar Matthieu Sozeau2017-12-01
| |_|/ / / / |/| | | | |
| | | * | | Documenting the -Q flag of coqchk.Gravatar Pierre-Marie Pédrot2017-12-01
| | | | | |
* | | | | | Merge PR #6276: Coqchk accepts filenamesGravatar Maxime Dénès2017-12-01
|\ \ \ \ \ \ | |_|/ / / / |/| | / / / | | |/ / / | |/| | |
| * | | | Documenting the possibility to pass filenames to coqchk.Gravatar Pierre-Marie Pédrot2017-11-29
| | |/ / | |/| |
| | * | use \ocaml macro in new textGravatar Paul Steckler2017-11-28
| | | |
* | | | Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gravatar Gaëtan Gilbert2017-11-28
|/ / /
* | | Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\ \ \
* | | | Updating the current official writing of OCaml, updating Camlp4->Camlp5.Gravatar Hugo Herbelin2017-11-25
| | | |
| * | | Allow local universe renaming in Print.Gravatar Gaëtan Gilbert2017-11-25
|/ / /
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 21:21:11 +0000