aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
Commit message (Collapse)AuthorAge
* 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
* | | | [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
|/ /
* | Allow local universe renaming in Print.Gravatar Gaëtan Gilbert2017-11-25
| |
| * use OCaml criteria for infix ops, #6212Gravatar Paul Steckler2017-11-22
|/
* Rename coq-inferior.el -> inferior-coq.el to match provided feature.Gravatar Gaëtan Gilbert2017-11-19
| | | | Fixes #4988.
* coq_makefile: document COQ_SRC_SUBDIRSGravatar Enrico Tassi2017-11-13
|
* Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]",Gravatar Samuel Gruetter2017-11-06
| | | | | | not "first [ progress tac1 | progress tac2 ]". And add a missing backslash.
* Merge PR #1139: Add a linter.Gravatar Maxime Dénès2017-11-06
|\
* \ Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631Gravatar Maxime Dénès2017-10-27
|\ \
* | | Rename \Tree to \NatTreeGravatar Johannes Kloos2017-10-25
| | |
| | * Put newlines at the end of files.Gravatar Gaëtan Gilbert2017-10-25
| | |
* | | Fix #5763: Strictly positive example is out of order.Gravatar jkloos2017-10-24
| | | | | | | | | | | | | | | | | | I also renamed the type to nattree (see discussion on https://github.com/coq/coq/pull/5979) to disambiguate from another, earlier example.
| * | Fix #4846Gravatar Johannes Kloos2017-10-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | Bug description: The "now" tactic, which is being used in the standard library, is not documented in the Reference Manual This commit documents the easy tactic, and gives now as a variant.
| * | Fix #5413: [unfold ... in] not documentedGravatar Johannes Kloos2017-10-24
| | | | | | | | | | | | Made a description of unfold...in and moved the index entry there.
| * | Documentation: Add various basic constructs to the index.Gravatar Johannes Kloos2017-10-24
| | | | | | | | | | | | | | | This was mentioned in #5631 as well. Now, forall, fun and casts have index entries.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 17:50:19 +0000