| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-11-03 | Lets Hints/Instances take an optional pattern | Matthieu Sozeau | |
| In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well. | |||
| 2016-11-03 | Document options of typeclasses (eauto) | Matthieu Sozeau | |
| With update after J. Gross comments | |||
| 2016-10-29 | Documenting changes in typeclasses | Matthieu Sozeau | |
| 2016-10-25 | Remove v62 from the refman. | Théo Zimmermann | |
| 2016-10-24 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-24 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-19 | Documenting Hint Resolve -> and <- variants. | Théo Zimmermann | |
| These variants are from 8.3 but were never documented except in CHANGES. | |||
| 2016-10-19 | Making the doc of auto hints more precise. | Théo Zimmermann | |
| The doc of auto hints now mention again that sometimes a hint will be used with simple apply and sometimes it will be used with exact. It does not try to be fully precise in that we don't necessarily want to document the behaviors of auto that we might like to change. See also the discussion on commit 9227d6e. | |||
| 2016-10-18 | Extending the doc with a general summary of auto variants. | Théo Zimmermann | |
| This way of giving the summary avoids redundancy as much as possible. It is helpful for the auto-completion of Company-Coq of @cpitclaudel. | |||
| 2016-10-18 | Document info_auto. | Théo Zimmermann | |
| Now that this tactic has been fixed (commit 58d1381), it needed to get documented. | |||
| 2016-10-18 | Improve the documentation of eauto. | Théo Zimmermann | |
| Improve the description of what auto/eauto do. These two tactics rely on the simple version of apply/eapply. Since this simple version is available to the end user, it is better to mention it. See also the confusion that such description can create in the thread "Understanding auto" on Coq-Club. | |||
| 2016-10-05 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 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-10-02 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 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.6' | Pierre-Marie Pédrot | |
| 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-14 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-09-12 | Refolding: disable in 8.4 compat file, document | Matthieu Sozeau | |
| 2016-09-08 | Merge PR #244. | Pierre-Marie Pédrot | |
| 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-19 | Remove errorlabstrm in favor of user_err | Emilio Jesus Gallego Arias | |
| 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. | |||
| 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-06 | Fix #4793: Coq 8.6 should accept -compat 8.6 | Maxime Dénès | |
| We also add a Coq86.v compat file. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |