| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | Not using style tags when translating/beautifying a file. | Hugo Herbelin | |
| 2016-11-05 | Removing a special treatment for empty lines in comments. | Hugo Herbelin | |
| This made the whole pp code complicated only for the purpose of the beautifier, while it is not clear when this was useful. Removing the code for simplicity, not excluding to later address beautifier issues when they show up. | |||
| 2016-11-05 | Removing obsolete parsing of strings à la v7 in comments. | Hugo Herbelin | |
| This was for the translator and is not relevant for the beautifier. | |||
| 2016-11-05 | Credits for 8.6 | Matthieu Sozeau | |
| 2016-11-05 | Minor fix in documentation | Matthieu Sozeau | |
| 2016-11-05 | Do not print dependent evars by default (expensive) | Matthieu Sozeau | |
| The option can be turned on by the user though. | |||
| 2016-11-05 | More precise refine compatibility | Matthieu Sozeau | |
| 2016-11-04 | Quick fix of tactic parsing while Load-ing in coqide. | Hugo Herbelin | |
| Note that this is still broken when loading files containing C-zar scripts. | |||
| 2016-11-04 | Test for #4966 ("auto" wrongly seen as "auto with *" when in position of ident). | Hugo Herbelin | |
| 2016-11-04 | Fix #3441 Use pf_get_type_of to avoid blowup | Matthieu Sozeau | |
| ... in pose proof of large proof terms | |||
| 2016-11-04 | Fix refine in compatibility mode | Matthieu Sozeau | |
| 2016-11-04 | Fix #4837: ./configure -local makes coqdep issue many warnings | Maxime Dénès | |
| We simply remove the warnings about paths mixing Win32 and Unix separators, since that situation does not seem problematic (c.f. discussion on the bug tracker). | |||
| 2016-11-04 | Merge remote-tracking branch 'github/pr/335' into v8.6 | Maxime Dénès | |
| Was PR#335: Fix printing of typeclasses eauto debug wrt intro. | |||
| 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-04 | Silence option deprecation warnings in the compat file | Jason Gross | |
| Some options are expected to be deprecated | |||
| 2016-11-03 | Remove an OCaml 4.02 construct. | Maxime Dénès | |
| This was not detected by running coq-contribs, so it probably means that we are not testing with the right version of OCaml. | |||
| 2016-11-03 | Merge remote-tracking branch 'github/pr/340' into v8.6 | Maxime Dénès | |
| Was PR#340: Fix various shortcomings of the warnings infrastructure. | |||
| 2016-11-03 | Rework search_strategy option handling | Matthieu Sozeau | |
| 2016-11-03 | Internal API change to typeclasses eauto. | Théo Zimmermann | |
| This commit makes the traversing strategy of typeclasses eauto an optional argument of the function that implements it. This change should be non-breaking. | |||
| 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 | Fix test-suite files relying on tcs bugs | Matthieu Sozeau | |
| - One was expecting shelved goals to remain after resolution (from refine). - The other too were relying on the wrong classification of subgoals as typeclass subgoals at toplevel. | |||
| 2016-11-03 | Fixed bug #4095. | Matthieu Sozeau | |
| 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 | Fix [typeclasses eauto with] and nopattern hints | Matthieu Sozeau | |
| This was the source of a bug in #5115#c7. | |||
| 2016-11-03 | Fix handling of only_classes at toplevel | Matthieu Sozeau | |
| 2016-11-03 | Test new syntax for hints and typeclass options | Matthieu Sozeau | |
| 2016-11-03 | Handle Unique Solutions flag. | Matthieu Sozeau | |
| 2016-11-03 | TCS: error handling and debug printing in resolution | Matthieu Sozeau | |
| 2016-11-03 | Fix bugs in Filtered Unification and cleanup code | Matthieu Sozeau | |
| 2016-11-03 | Fix Typeclasses eauto := bfs. | Matthieu Sozeau | |
| 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-11-03 | Merge remote-tracking branch 'github/pr/341' into v8.6 | Maxime Dénès | |
| Was PR#341: Better Arguments compatibility. | |||
| 2016-11-02 | Better Arguments compatibility. | Maxime Dénès | |
| With multiple arguments list, repeating the "/" modifier used to be mandatory. So instead of forbidding it, we issue a deprecation warning. | |||
| 2016-11-02 | Fix various shortcomings of the warnings infrastructure. | Maxime Dénès | |
| - The flags are now interpreted from left to right, without any other precedence rule. The previous one did not make much sense in interactive mode. - Set Warnings and Set Warnings Append are now synonyms, and have the "append" semantics, which is the most natural one for warnings. - Warnings on unknown warnings are now printed only once (previously the would be repeated on further calls to Set Warnings, sections closing, module requiring...). - Warning status strings are normalized, so that e.g. "+foo,-foo" is reduced to "-foo" (if foo exists, "" otherwise). | |||
| 2016-11-02 | Put string between quotes when printing an option value. | Maxime Dénès | |
| This is a better (more generic) fix to #5061 than my e8b9ee76. | |||
| 2016-10-30 | Fix spurious OCaml Warning 56 in TACTIC EXTEND macros. | Pierre-Marie Pédrot | |
| 2016-10-29 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-10-29 | Removing dead code. | Hugo Herbelin | |
| 2016-10-29 | Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c). | Hugo Herbelin | |
| (May it fell in the case mentioned in the inner comment of Exninfo.info?) | |||
| 2016-10-29 | Documenting changes in typeclasses | Matthieu Sozeau | |
| 2016-10-29 | Fixing #5164 (regression in locating error in argument of "refine"). | Hugo Herbelin | |
| Reporting location was not expecting a term passed to an ML tactic to be interpreted by the ML tactic itself. Made an empirical fix to report about the as-precise-as-possible location available. | |||
| 2016-10-28 | Merge remote-tracking branch 'github/pr/321' into v8.6 | Maxime Dénès | |
| Was PR#321: Handling of section variables in hints | |||
| 2016-10-28 | Merge remote-tracking branch 'github/pr/319' into v8.6 | Maxime Dénès | |
| Was PR#319: More error tagging, try to fix bug 5135 | |||
| 2016-10-28 | Merge commit 'fccbd64' into v8.6 | Maxime Dénès | |
| Was PR#187: Add a META file to support ocamlfind linking. | |||
| 2016-10-28 | [build] Add a target to install the META file. | Emilio Jesus Gallego Arias | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |