| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-10-03 | fixing bug 4609: document an option governing the generation of equalities | Yves Bertot | |
| between proofs in tactic injection, with a side-effect on inversion. | |||
| 2016-09-30 | Merge remote-tracking branch 'github/pr/280' into v8.6 | Maxime Dénès | |
| Was PR#280: Document that [Reset Ltac Profile] is not synchronized with the document state | |||
| 2016-09-30 | Merge branch 'v8.5' into v8.6 | Maxime Dénès | |
| 2016-09-28 | Merge remote-tracking branch 'github/pr/232' into v8.6 | Maxime Dénès | |
| Was PR#232: Fix the parsing of goal selectors. | |||
| 2016-09-27 | Fixing #4887 (confusion between using and with in documentation of firstorder). | Hugo Herbelin | |
| 2016-09-23 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-19 | Replace { command ; } with ( command ) | Erik Martin-Dorel | |
| as suggested by Hugo. Also, escape the spaces after the dots to obtain a better PdfLaTeX output. | |||
| 2016-09-19 | Fix typos in RefMan-uti.tex. | Erik Martin-Dorel | |
| - Ensure "coq_makefile --help" is properly typeset with HeVeA/PdfLaTeX - Replace 's with "s so they are typeset as true ASCII characters - Add missing ; before closing brace. | |||
| 2016-09-16 | Doc: [Reset Ltac Profile] is not synchronized | Jason Gross | |
| 2016-09-15 | Extending "contradiction" so that it recognizes statements such as "~x=x" or ↵ | Hugo Herbelin | |
| ~True. Found 1 incompatibility in tested contribs and 3 times the same pattern of incompatibility in the standard library. In all cases, it is an improvement in the form of the script. New behavior deactivated when version is <= 8.5. | |||
| 2016-09-12 | Refolding: disable in 8.4 compat file, document | Matthieu Sozeau | |
| 2016-09-07 | Fix a typo in the reference manual | Jason Gross | |
| 2016-08-30 | plugin micromega : nra also handles non-linear rational arithmetic over Q ↵ | Frédéric Besson | |
| (Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R. | |||
| 2016-08-23 | update Proof General URL | Paul Steckler | |
| 2016-08-21 | Documenting "Set Structural Injection". | Hugo Herbelin | |
| 2016-08-17 | In docs, fix command to reset Ltac profiling | Paul Steckler | |
| 2016-08-16 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-08-04 | Fix documentation typo (bug #4994). | Guillaume Melquiond | |
| 2016-07-17 | More examples of recursive notations, with emphasis in reference manual. | Hugo Herbelin | |
| 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) ..) ..). | |||
| 2016-07-01 | Add and document match, fix and cofix reduction flags. | Maxime Dénès | |
| 2016-06-30 | Update the documentation for goal selectors. | Cyprien Mangin | |
| 2016-06-29 | Updated CHANGES about subst. More on recursive equations in reference manual. | Hugo Herbelin | |
| 2016-06-29 | Fixes in documentation. | Matthieu Sozeau | |
| 2016-06-29 | Program: cleanup in cases, add options | Matthieu Sozeau | |
| Unset Program Generalized Coercion to avoid coercion of general applications. Unset Program Cases to deactivate generation equalities and disequalities of cases. | |||
| 2016-06-28 | Merge remote-tracking branch 'github/pr/207' into trunk | Maxime Dénès | |
| Was PR#207: Add -no-print-dependent-evars | |||
| 2016-06-28 | Documenting the "only printing" notation flag. | Pierre-Marie Pédrot | |
| 2016-06-27 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-06-27 | Adding ability to put any pattern in binders, prefixed by a quote. | Daniel de Rauglaudre | |
| Cf CHANGES for details. | |||
| 2016-06-20 | Reference Manual / Extraction: the original example command no longer works ↵ | Matej Kosik | |
| with recent Coq | |||
| 2016-06-19 | Add [Unset Printing Dependent Evars Line] | Jason Gross | |
| This allows a work-around for bug #4819, https://coq.inria.fr/bugs/show_bug.cgi?id=4819. | |||
| 2016-06-17 | par: like all: but in parallel | Enrico Tassi | |
| 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. | |||
| 2016-06-16 | Document new Hint Mode option. | Matthieu Sozeau | |
| 2016-06-16 | Revise syntax of Hint Cut | Matthieu Sozeau | |
| As noticed by C. Cohen it was confusingly different from standard notation. | |||
| 2016-06-16 | Merge 'pr/191' into trunk | Enrico Tassi | |
| 2016-06-15 | typography | Matej Kosik | |
| 2016-06-14 | Add documentation for goal selectors. | Cyprien Mangin | |
| 2016-06-14 | -async-proofs-delegation-threshold default value set to 0.03 | Enrico Tassi | |
| Documentation also updated. | |||
| 2016-06-14 | Merge remote-tracking branch 'origin/pr/173' into trunk | Enrico Tassi | |
| This is the "error resiliency" mode for STM | |||
| 2016-06-14 | Merge branch "LtacProf for trunk" (PR #165). | Pierre-Marie Pédrot | |
| 2016-06-13 | Univs: more robust Universe/Constraint decls #4816 | Matthieu Sozeau | |
| 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 | |||
| 2016-06-07 | typo | Matej Kosik | |
| 2016-06-07 | typography | Matej Kosik | |
| 2016-06-07 | Documentation | Enrico Tassi | |
| 2016-06-05 | Make Ltac Profiling an setting | Jason Gross | |
| 2016-06-05 | Synchronize the profiler state with the document | Jason Gross | |
| 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. | |||
| 2016-06-05 | -profileltac -> -profile-ltac, as per @herbelin | Jason Gross | |
| https://github.com/coq/coq/pull/150#issuecomment-219141596 ```bash git grep --name-only profileltac | xargs sed s'/profileltac/profile-ltac/g' -i ``` | |||
| 2016-06-05 | Add LtacProf documentation | Jason Gross | |
| 2016-06-05 | Adding the Print Ltac Signature command. | Pierre-Marie Pédrot | |
| 2016-05-15 | Fix a really small doc typo | Ricky Elrod | |
| 2016-05-04 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |