aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
* | plugin micromega : nra also handles non-linear rational arithmetic over Q ↵Gravatar Frédéric Besson2016-08-30
| | | | | | | | | | | | | | (Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R.
* | update Proof General URLGravatar Paul Steckler2016-08-23
| |
* | Documenting "Set Structural Injection".Gravatar Hugo Herbelin2016-08-21
| |
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | | | | | | | As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch.
* | In docs, fix command to reset Ltac profilingGravatar Paul Steckler2016-08-17
|/
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\
| * Fix documentation typo (bug #4994).Gravatar Guillaume Melquiond2016-08-04
| |
* | More examples of recursive notations, with emphasis in reference manual.Gravatar Hugo Herbelin2016-07-17
| | | | | | | | | | | | | | | | | | | | | | | | | | Further work would include: - Identify binders up to alpha-conversion (see #4932 with a list of binders of length at least 2, or #4592 on printing notations such as ex2). A cool example that one could also consider supporting: - Notation "[[ a , .. , b | .. | a , .. , b ]]" := (cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..).
* | Fix #4793: Coq 8.6 should accept -compat 8.6Gravatar Maxime Dénès2016-07-06
| | | | | | | | We also add a Coq86.v compat file.
* | Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
| |
* | Updated CHANGES about subst. More on recursive equations in reference manual.Gravatar Hugo Herbelin2016-06-29
| |
* | Fixes in documentation.Gravatar Matthieu Sozeau2016-06-29
| |
* | Program: cleanup in cases, add optionsGravatar Matthieu Sozeau2016-06-29
| | | | | | | | | | | | | | Unset Program Generalized Coercion to avoid coercion of general applications. Unset Program Cases to deactivate generation equalities and disequalities of cases.
* | Merge remote-tracking branch 'github/pr/207' into trunkGravatar Maxime Dénès2016-06-28
|\ \ | | | | | | | | | Was PR#207: Add -no-print-dependent-evars
* | | Documenting the "only printing" notation flag.Gravatar Pierre-Marie Pédrot2016-06-28
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\ \ \ | | |/ | |/|
* | | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| | | | | | | | | | | | Cf CHANGES for details.
| * | Reference Manual / Extraction: the original example command no longer works ↵Gravatar Matej Kosik2016-06-20
| | | | | | | | | | | | with recent Coq
| | * Add [Unset Printing Dependent Evars Line]Gravatar Jason Gross2016-06-19
| |/ |/| | | | | | | This allows a work-around for bug #4819, https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
* | par: like all: but in parallelGravatar Enrico Tassi2016-06-17
| | | | | | | | | | | | | | | | | | | | | | | | | | This commit documents par:, fixes its semantics so that is behaves like all:, supports (toplevel) abstract and optimizes toplevel solve. `par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1` but is optimized for failures: if one goal fails all are aborted immediately. `par: abstract tac` runs abstract on the generated proof terms. Nested abstract calls are not supported.
* | Document new Hint Mode option.Gravatar Matthieu Sozeau2016-06-16
| |
* | Revise syntax of Hint CutGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | As noticed by C. Cohen it was confusingly different from standard notation.
* | Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\ \
* | | typographyGravatar Matej Kosik2016-06-15
| | |
| * | Add documentation for goal selectors.Gravatar Cyprien Mangin2016-06-14
| | |
* | | -async-proofs-delegation-threshold default value set to 0.03Gravatar Enrico Tassi2016-06-14
| | | | | | | | | | | | Documentation also updated.
* | | Merge remote-tracking branch 'origin/pr/173' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ | |/ / |/| | | | | This is the "error resiliency" mode for STM
* | | Merge branch "LtacProf for trunk" (PR #165).Gravatar Pierre-Marie Pédrot2016-06-14
|\ \ \
* | | | Univs: more robust Universe/Constraint decls #4816Gravatar Matthieu Sozeau2016-06-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes the declarations of constraints, universes and assumptions: - global constraints can refer to global universes only, - polymorphic universes, constraints and assumptions can only be declared inside sections, when all the section's variables/universes are polymorphic as well. - monomorphic assumptions may only be declared in section contexts which are not parameterized by polymorphic universes/assumptions. Add fix for part 1 of bug #4816
* | | | typoGravatar Matej Kosik2016-06-07
| | | |
* | | | typographyGravatar Matej Kosik2016-06-07
| | | |
| | * | DocumentationGravatar Enrico Tassi2016-06-07
| |/ / |/| |
| * | Make Ltac Profiling an settingGravatar Jason Gross2016-06-05
| | |
| * | Synchronize the profiler state with the documentGravatar Jason Gross2016-06-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | This is suboptimal, because mutation leaves room for subtle bugs, but rewriting @tebbi's code to be functional was a pain, and not something I could figure out how to do easily. I'm working under the assumption that there is no sharing in a single treenode, which I'm not completely sure is valid. That said, a few simple tests seem to indicate that this works as expected.
| * | -profileltac -> -profile-ltac, as per @herbelinGravatar Jason Gross2016-06-05
| | | | | | | | | | | | | | | | | | | | | | | | https://github.com/coq/coq/pull/150#issuecomment-219141596 ```bash git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i ```
| * | Add LtacProf documentationGravatar Jason Gross2016-06-05
|/ /
* | Adding the Print Ltac Signature command.Gravatar Pierre-Marie Pédrot2016-06-05
| |
* | Fix build of documentation (broken for four months).Gravatar Guillaume Melquiond2016-06-03
| |
* | Fix a really small doc typoGravatar Ricky Elrod2016-05-15
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\|
| * In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | preserved, which is a source of incompatibilities w.r.t. released 8.5 but which looks to me to be the only possible canonical behavior. This is I believe a better behavior than the Regular Subst Tactic behavior in the released 8.5 and 8.5pl1. There, the order of hypotheses in which substitutions happened was respected, but their interleaving with other hypotheses was not respected. So, I consider this to be a fix to the "Regular Subst Tactic" mode. Also added a more detailed "specification" of the "Regular" behavior of "subst" in the reference manual.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-02
|\|
| * Update tutorial (fix bug #4699).Gravatar Guillaume Melquiond2016-04-28
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\|
| * FIX: HTML version of Chapter 4 of the Reference ManualGravatar Matej Kosik2016-04-12
| |
| * TYPOGRAPHY: adding missing \noindent macrosGravatar Matej Kosik2016-04-12
| |
* | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵Gravatar Matthieu Sozeau2016-04-04
|\ \ | | | | | | | | | into JasonGross-trunk-function_scope
* \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\ \ \ | | |/ | |/|
| * | Document Hint Mode, cleanup Hint doc.Gravatar Matthieu Sozeau2016-02-24
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 19:39:38 +0000