| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-11-15 | Revert part of a477dc, disallow_shelved | Matthieu Sozeau | |
| In only_classes mode we do not try to implement a stricter semantics for shelved goals in 8.6. Leaving this for 8.7. Update the documentation as well. Remove a spurious printf call as well. Fix test-suite now that shelved goals are allowed | |||
| 2016-11-14 | Do not mention "none" in warnings doc, as it is there for compatibility. | Maxime Dénès | |
| 2016-11-10 | Update CHANGES and credits for 8.6beta1. | Maxime Dénès | |
| 2016-11-08 | Merge remote-tracking branch 'github/pr/348' into v8.6 | Maxime Dénès | |
| Was PR#348: Credits for 8.6 | |||
| 2016-11-08 | Update documentation of Arguments after recent changes. | Maxime Dénès | |
| 2016-11-08 | Rewording from Enrico | Matthieu Sozeau | |
| 2016-11-07 | After Emilio's comment. | Matthieu Sozeau | |
| 2016-11-07 | Merge remote-tracking branch 'github/pr/339' into v8.6 | Maxime Dénès | |
| Was PR#339: Documenting type class options, typeclasses eauto | |||
| 2016-11-07 | Document two new variants of refine | Matthieu Sozeau | |
| They allow to call refine without doing typeclass resolution, allowing to use refine in typeclass hints. | |||
| 2016-11-07 | More accurate contributor list. | Matthieu Sozeau | |
| Command used: git log v8.5..HEAD --pretty=format:"%an," | sort -k 2 | uniq with some manual postprocessing for login names, particles and multiple first names. | |||
| 2016-11-07 | Hugo and Maxime's 2nd pass of comments | Matthieu Sozeau | |
| 2016-11-06 | Hugo's comments | Matthieu Sozeau | |
| 2016-11-06 | Maxime's comments | Matthieu Sozeau | |
| 2016-11-06 | Fixes from Enrico's review | Matthieu Sozeau | |
| 2016-11-05 | Credits for 8.6 | Matthieu Sozeau | |
| 2016-11-05 | Minor fix in documentation | Matthieu Sozeau | |
| 2016-11-04 | Merge remote-tracking branch 'github/pr/336' into v8.6 | Maxime Dénès | |
| Was PR#336: Remove v62 | |||
| 2016-11-04 | Add documentation for [Set Warnings] and the -w option. | Cyprien Mangin | |
| 2016-11-03 | Do not shelve non-class subgoals but fail, it should | Matthieu Sozeau | |
| be the instance writer's responsibility to not generated non-dependent non-class subgoals (otherwise we loose compatibility as shown in e.g. MathClasses, which goes into loops because of unexpectedly unconstrained goals). Reflect it in the doc. | |||
| 2016-11-03 | typeclasses eauto Implem/doc of shelving strategy | Matthieu Sozeau | |
| Now [typeclasses eauto] mimicks what happens during resolution faithfully, and the shelving behavior/requirements for a successful proof-search are documented. | |||
| 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.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-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-06 | Fix #4793: Coq 8.6 should accept -compat 8.6 | Maxime Dénès | |
| We also add a Coq86.v compat file. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |