| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Merge PR#713: Bump year in headers. |  Maxime Dénès | 2017-06-15 |
| |\ | |||
| * \ | Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraints | Maxime Dénès | 2017-06-15 |
| |\ \ | |||
| * | | | Fix Bug #5568, no dup notation warnings on repeated module imports |  Paul Steckler | 2017-06-09 |
| | | | | |||
| | * | | Univs: fix bug #5365, generation of u+k <= v constraints |  Matthieu Sozeau | 2017-06-05 |
| | | | | | | | | | | | | | Use an explicit label ~algebraic for make_flexible_variable as well. | ||
| * | | | Merge PR#631: Fix bug #5255 | Maxime Dénès | 2017-06-01 |
| |\ \ \ | |||
| | | | * | Bump year in headers. | Maxime Dénès | 2017-06-01 |
| | |_|/ |/| | | |||
| * | | | Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show Match | Maxime Dénès | 2017-05-28 |
| |\ \ \ | |||
| * \ \ \ | Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if ↵ | Maxime Dénès | 2017-05-26 |
| |\ \ \ \ | | | | | | | | | | | | | | | | printing only | ||
| | | * | | | Bug 5546, qualify datatype constructors when needed | Paul Steckler | 2017-05-25 |
| | |/ / / |/| | | | |||
| | * | | | Fixing bug #5526,allow nonlinear variables in Notation patterns | Paul Steckler | 2017-05-17 |
| | | | | | |||
| | | * | | Fix #5255: [Context (x : T := y)] should mean [Let x := y]. |  Pierre-Marie Pédrot | 2017-05-15 |
| | |/ / | |||
| * / / | Removing a variable warned unused. |  Hugo Herbelin | 2017-05-14 |
| |/ / | |||
| * | | Merge PR#604: FIx bug #5300: Anomaly: Uncaught exception Not_found" in ↵ | Maxime Dénès | 2017-05-10 |
| |\ \ | | | | | | | | | | "Print Assumptions". | ||
| * | | | Fix bug #3659: -time should understand multibyte encodings. | Pierre-Marie Pédrot | 2017-05-05 |
| | | | | | | | | | | | | | | | | We assume Coq always outputs UTF-8 (is it really the case?) and cut strings after 30 UTF-8 characters instead of using the standard String function. | ||
| | * | | FIx bug #5300: uncaught exception in "Print Assumptions". |  Cyprien Mangin | 2017-05-03 |
| |/ / | |||
| * | | Fixing bug #5470 (anomaly on notations with misused "binder" type). | Hugo Herbelin | 2017-04-14 |
| | | | |||
| * | | Fixing bug #5469 (notation format not recognizing curly braces). | Hugo Herbelin | 2017-04-14 |
| | | | |||
| * | | Fix a few programming pearls related to Time, Fail and Redirect. | Maxime Dénès | 2017-04-06 |
| | | | | | | | | | | | | | | | | | | | This fixes a few clear bugs, but the STM code handling Time, Fail and Redirect before par: still needs to be rewritten. It does not implement the same semantics as the vernac interpreter for Fail Fail [c] and ignores Redirect. This commit was already reviewed with Enrico and tested on Travis. | ||
| * | | Merge branch 'origin/v8.5' into v8.6. | Hugo Herbelin | 2017-04-06 |
| |\ \ | | | | | | | | | | Was needed to be done for a while. | ||
| * | | | Instances should obey universe binders even when defined by tactics. |  Gaetan Gilbert | 2017-04-03 |
| | | | | |||
| * | | | Merge PR#429: Don't require printing-only notation to be productive | Maxime Dénès | 2017-03-17 |
| |\ \ \ | |_|/ |/| | | |||
| | | * | Fixing a little bug in using the "where" clause for inductive types. | Hugo Herbelin | 2017-02-23 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This was not working when the inductive type had implicit parameters. This could still be improved. E.g. the following still does not work: Reserved Notation "#". Inductive I {A:Type} := C : # where "#" := I. But it should be made working by taking care of adding the mandatory implicit argument A at the time # is interpreted as [@I _] (i.e., technically speaking, using expl_impls in interp_notation). | ||
| * | | | Fixing #5339 (anomaly with 'pat in record parameters). | Hugo Herbelin | 2017-02-16 |
| | | | | |||
| | * | | reject notations that are both 'only printing' and 'only parsing' |  Ralf Jung | 2017-02-16 |
| | | | | |||
| | * | | don't require printing-only notation to be productive | Ralf Jung | 2017-02-16 |
| |/ / | |||
| * | | Fix bug #5262: Error should tell me which name is duplicated. | Pierre-Marie Pédrot | 2017-01-28 |
| | | | |||
| * | | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | 2017-01-23 |
| |\| | |||
| * | | Fixing (part of) #5303 (clarifications around Record/Structure/Variant). | Hugo Herbelin | 2017-01-16 |
| | | | | | | | | | | | | | - We fix the inconsistency of Structure and Record which according to doc are the same. - We improve the error message when not using { ... } for Record or Structure. | ||
| | * | Fix some documentation typos. |  Guillaume Melquiond | 2016-12-26 |
| | | | |||
| | * | Excluding explicitly coinductive types in Scheme Equality (#5284). | Hugo Herbelin | 2016-12-23 |
| | | | |||
| | * | Fixing anomaly EqUnknown in Equality Scheme (#5278). | Hugo Herbelin | 2016-12-22 |
| | | | |||
| * | | Merge remote-tracking branch 'github/pr/366' into v8.6 | Maxime Dénès | 2016-12-04 |
| |\ \ | | | | | | | | | | Was PR#366: Univs: fix bug 5208 | ||
| * | | | Comment on universe handling in Parameters |  Matthieu Sozeau | 2016-12-02 |
| | | | | |||
| * | | | Univs: fix bug #5188 | Matthieu Sozeau | 2016-12-02 |
| | | | | | | | | | | | | | | | | Parameter was implemented the wrong way trying to separate the universes of the telescope. | ||
| | * | | Fix UGraph.check_eq! | Matthieu Sozeau | 2016-11-30 |
| |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Universes are kept in normal form w.r.t. equality but not the <= relation, so the previous check worked almost always but was actually too strict! In cases like (max(Set,u) = u) when u is declared >= Set it was failing to find an equality. Applying the KISS principle: u = v <-> u <= v /\ v <= u. Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of a colon in a typing judgment), this was not the case when an algebraic universe instantiated an evar that appeared in the term. We force their universe variable status to change in refresh_universes to avoid this. Fix ind sort inference: Use syntactic universe equality for inductive sort inference instead of check_leq (which now correctly takes constraints into account) and simplify code | ||
| * | | Fix some documentation typos. | Guillaume Melquiond | 2016-11-24 |
| | | | | | | | | | | | Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else. | ||
| * | | Stop parsing -compat-notations options, which are no longer supported (bug ↵ | Guillaume Melquiond | 2016-11-21 |
| | | | | | | | | | #3339). | ||
| * | | Revert "Merge remote-tracking branch 'github/pr/360' into v8.6" | Maxime Dénès | 2016-11-18 |
| | | | | | | | | | | | | | | | | | | | This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341. It turns out that calling from fake_ide the STM commands that were removed by this PR requires an extension of the XML protocol. So postponing the integration. | ||
| * | | [stm] Remove STM-related vernaculars |  Emilio Jesus Gallego Arias | 2016-11-17 |
| | | | | | | | | | | | | | | | | | | | I think these commands never make a lot of sense on scripts other than debugging and we have better methods now. The last remaining command, used for the tty emulation has been renamed to VtBack, but it should go away at some point too once the legacy interfaces are removed. | ||
| * | | Fix bug in warnings: -w foo was silent when foo did not exist. | Maxime Dénès | 2016-11-14 |
| | | | |||
| * | | Do not mention "none" in warnings doc, as it is there for compatibility. | Maxime Dénès | 2016-11-14 |
| | | | |||
| * | | Merge remote-tracking branch 'github/pr/339' into v8.6 | Maxime Dénès | 2016-11-07 |
| |\ \ | | | | | | | | | | Was PR#339: Documenting type class options, typeclasses eauto | ||
| | * | | Fixes to compile with ocaml 4.01 | Matthieu Sozeau | 2016-11-07 |
| | | | | |||
| * | | | Merge commit 'e6edb33' into v8.6 | Maxime Dénès | 2016-11-07 |
| |\ \ \ | | | | | | | | | | | | | Was PR#331: Solve_constraints and Set Use Unification Heuristics | ||
| * | | | | Improve formatting of a message in [Arguments]. | Maxime Dénès | 2016-11-07 |
| | | | | | |||
| * | | | | Fix #5181: [Arguments] no longer correctly checks the length of arguments lists | Maxime Dénès | 2016-11-07 |
| | | | | | |||
| * | | | | Fix #5182: "Arguments names must be distinct." is bogus and underinformative | Maxime Dénès | 2016-11-07 |
| | | | | | |||
| * | | | | Not using style tags when translating/beautifying a file. | Hugo Herbelin | 2016-11-05 |
| | | | | | |||
| * | | | | Quick fix of tactic parsing while Load-ing in coqide. | Hugo Herbelin | 2016-11-04 |
| | | | | | | | | | | | | | | | | | Note that this is still broken when loading files containing C-zar scripts. | ||
| * | | | | Add documentation for [Set Warnings] and the -w option. | Cyprien Mangin | 2016-11-04 |
| | | | | | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |