| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-01-12 | Reporting about the new tactical unshelve. | Hugo Herbelin | |
| 2015-12-17 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-16 | Update version numbers and magic numbers for 8.5rc1 release. | Maxime Dénès | |
| 2015-12-16 | Add a "simple refine" variant of "refine" that does not call "shelve_unifiable". | Guillaume Melquiond | |
| 2015-12-15 | Proof using: do not clear unused section hyps automatically | Enrico Tassi | |
| The option is still there, but not documented since it is too dangerous. Hints and type classes instances are not taking cleared variables into account. | |||
| 2015-12-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-14 | Updating CHANGES with an incompatibility. | Hugo Herbelin | |
| 2015-12-14 | Flag -compat 8.4 now loads Coq.Compat.Coq84. | Maxime Dénès | |
| 2015-12-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-11 | Document removal of Set Virtual Machine and -vm in CHANGES. | Maxime Dénès | |
| 2015-12-10 | Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn. | Hugo Herbelin | |
| Marking it as experimental. | |||
| 2015-12-08 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-05 | Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction) | Hugo Herbelin | |
| based on a suggestion of Guillaume M. (done like this in ssreflect). This is actually consistent with the hack of using "destruct (1)" to mean the term 1 by opposition to the use of "destruct 1" to mean the first non-dependent hypothesis of the goal. | |||
| 2015-12-05 | Fix CHANGES. | Hugo Herbelin | |
| 2015-12-03 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-12-02 | Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG. | Hugo Herbelin | |
| 2015-11-20 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-19 | Fix bug #4433, removing hack on evars appearing in a pattern from a | Matthieu Sozeau | |
| constr, and the associated signature, not needed anymore. Update CHANGES, no evar_map is produced by pattern_of_constr anymore. | |||
| 2015-11-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-12 | Update CHANGES | Jason Gross | |
| Mention compatibility file. | |||
| 2015-11-11 | Fix bug #3735: interpretation of "->" in Program follows the standard one. | Matthieu Sozeau | |
| 2015-11-10 | Listing separately changes from 8.5betas to final 8.5 and further | Hugo Herbelin | |
| changes from final 8.5 to next version. | |||
| 2015-11-10 | Activating bracketing of last or-and introduction pattern by default | Hugo Herbelin | |
| for more regularity. | |||
| 2015-11-05 | Update version numbers and magic numbers for 8.5beta3 release. | Maxime Dénès | |
| 2015-11-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-11-04 | Hint Cut documentation and cleanup of printing (was duplicated and | Matthieu Sozeau | |
| inconsistent). | |||
| 2015-11-02 | Adding syntax "Show id" to show goal named id (shelved or not). | Hugo Herbelin | |
| 2015-10-26 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-21 | Mention bug 3199 fix as a source of incompatibilities. | Matthieu Sozeau | |
| 2015-10-19 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-19 | Documenting the option "Strict Universe Declaration" in CHANGES. | Pierre-Marie Pédrot | |
| 2015-10-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond | |
| 2015-10-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-10-07 | Remove the "exists" overrides from Program. (Fix bug #4360) | Guillaume Melquiond | |
| 2015-10-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-09-28 | Make -load-vernac-object respect the loadpath. | Guillaume Melquiond | |
| This command-line option was behaving like the old -require, except that it did not do Import. In other words, it was loading files without respecting the loadpath. Now it behaves exactly like Require, while -require now behaves like Require Import. This patch also removes Library.require_library_from_file and all its dependencies, since they are no longer used inside Coq. | |||
| 2015-09-25 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-09-25 | The -require option now accepts a logical path instead of a physical one. | Pierre-Marie Pédrot | |
| 2015-09-25 | Updating the documentation and the toolchain w.r.t. the change in -compile. | Pierre-Marie Pédrot | |
| 2015-09-17 | Merge branch 'v8.5' into trunk | Maxime Dénès | |
| 2015-09-16 | Explain new flags for native_compute in CHANGES. | Maxime Dénès | |
| 2015-09-09 | Merge remote-tracking branch 'origin/v8.5' into trunk | Hugo Herbelin | |
| 2015-09-08 | New option "Unset Bracketing Last Introduction Pattern" for preserving | Hugo Herbelin | |
| compatibility with the non uniform behavior that "intros [] []" on "A*B->C*D->E" automatically introduces A and B but leaves C and D in the goal. Kept unset in 8.5 but planned to be set in 8.6. | |||
| 2015-09-08 | Documenting the new behaviour of the Shrink Obligations flag. | Pierre-Marie Pédrot | |
| 2015-08-22 | Documenting the Shrink Abstract option. | Pierre-Marie Pédrot | |
| 2015-08-14 | Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080 | Jason Gross | |
| This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change in the semantics of arguments scopes: scopes can no longer be bound to Funclass or Sortclass (this does not seem to be useful)). It is useful to have function_scope for, e.g., function composition. This allows users to, e.g., automatically interpret ∘ as morphism composition when expecting a morphism of categories, as functor composition when expecting a functor, and as function composition when expecting a function. Additionally, it is nicer to have fewer special cases in the OCaml code, and give more things a uniform syntax. (The scope type_scope should not be special-cased; this change is coming up next.) Also explicitly define [function_scope] in theories/Init/Notations.v. This closes bug #3080, Build a [function_scope] like [type_scope], or allow [Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass] We now mention Funclass and Sortclass in the documentation of [Bind Scope] again. | |||
| 2015-08-02 | Granting Jason's request for an ad hoc compatibility option on | Hugo Herbelin | |
| considering trivial unifications "?x = t" in tactics working under conjunctions (see #3545). Also updating and fixing wrong comments in test apply.v. | |||
| 2015-08-02 | Documenting change of behavior of apply when the lemma is a tuple and | Hugo Herbelin | |
| applying a component of the tuple. | |||
| 2015-07-10 | Rewording about how to upgrade on failing calls to constructor. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |