Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #7552: Fix #7539: Checker does not properly handle negative ↵ | 2018-06-04 | |
|\ | | | | | | | coinductive types. | ||
* | | Reduce circular dependency constants <-> projections | 2018-05-31 | |
| | | | | | | | | | | Instead of having the projection data in the constant data we have it independently in the environment. | ||
* | | Merge PR #7325: Fix #7323: coqchk puts polymorphic univs of inductive in ↵ | 2018-05-25 | |
|\ \ | | | | | | | | | | global env | ||
* \ \ | Merge PR #7177: Unifying names of "smart" combinators + adding combinators ↵ | 2018-05-24 | |
|\ \ \ | | | | | | | | | | | | | in CArray | ||
| | * | | Fix #7323: coqchk puts polymorphic univs of inductive in global env | 2018-05-24 | |
| |/ / |/| | | |||
* | | | Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constants | 2018-05-24 | |
|\ \ \ | |||
* \ \ \ | Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant ↵ | 2018-05-24 | |
|\ \ \ \ | | | | | | | | | | | | | | | | instances | ||
| | | * | | Moving Rtree.smart_map into Rtree.Smart.map. | 2018-05-23 | |
| | | | | | |||
| | | * | | Moving Option.smart_map to Option.Smart.map. | 2018-05-23 | |
| | | | | | |||
| | | * | | Collecting List.smart_* functions into a module List.Smart. | 2018-05-23 | |
| | | | | | |||
| | | * | | Collecting Array.smart_* functions into a module Array.Smart. | 2018-05-23 | |
| |_|/ / |/| | | | |||
| | | * | Fix #7539: Checker does not properly handle negative coinductive types. | 2018-05-18 | |
| | | | | | | | | | | | | | | | | | | | | The reduction machine of the checker was not taking into account the fact that cofixpoints needed to be unfolded when applied against a projection. | ||
* | | | | Infrastructure for ocamldebug on the checker | 2018-05-13 | |
| |_|/ |/| | | |||
| | * | Fix #7327: coqchk subtyping of polymorphic constants | 2018-04-23 | |
| |/ | |||
| * | Fix #6798: coqchk ignores ugraph when comparing constant instances | 2018-04-20 | |
|/ | |||
* | [api] Deprecate a couple of aliases that we missed. | 2018-03-28 | |
| | |||
* | Merge PR #6800: [checker] Printer cleanup. | 2018-03-09 | |
|\ | |||
* | | Update checker to reflect rule on constructors of polymorphic inductive types | 2018-03-08 | |
| | | |||
| * | [checker] Printer cleanup. | 2018-03-07 | |
|/ | | | | Makes printing rules more explicit and should close #6799. | ||
* | Replace invalid tag @raises in ocamldoc comments with @raise | 2018-03-05 | |
| | |||
* | Merge PR #6855: Update headers following #6543. | 2018-03-05 | |
|\ | |||
* \ | Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd) | 2018-02-28 | |
|\ \ | |||
| | * | Update headers following #6543. | 2018-02-27 | |
| |/ |/| | |||
* | | Merge PR #6740: Adding a sanity check on inductive variance subtyping. | 2018-02-21 | |
|\ \ | |||
* \ \ | Merge PR #6728: Extrude monomorphic universe contexts from with Definition ↵ | 2018-02-19 | |
|\ \ \ | | | | | | | | | | | | | constraints. | ||
* \ \ \ | Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵ | 2018-02-19 | |
|\ \ \ \ | | | | | | | | | | | | | | | | camlp4 | ||
| * | | | | Change references to CAMLP4 to CAMLP5 to be more accurate since we no | 2018-02-17 | |
| | | | | | | | | | | | | | | | | | | | | longer use camlp4. | ||
| | * | | | Extrude monomorphic universe contexts from with Definition constraints. | 2018-02-16 | |
| |/ / / |/| | | | | | | | | | | | | | | | We defer the computation of the universe quantification to the upper layer, outside of the kernel. | ||
| | * | | Adding a sanity check on inductive variance subtyping. | 2018-02-15 | |
| |/ / |/| | | |||
* | | | Merge PR #6262: [error] Replace msg_error by a proper exception. | 2018-02-12 | |
|\ \ \ | |||
| | | * | dest_{prod,lam}: no Cast case (it's removed by whd) | 2018-02-11 | |
| | |/ | |||
* | / | Simplification: cumulativity information is variance information. | 2018-02-10 | |
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since cumulativity of an inductive type is the universe constraints which make a term convertible with its universe-renamed copy, the only constraints we can get are between a universe and its copy. As such we do not need to be able to represent arbitrary constraints between universes and copied universes in a double-sized ucontext, instead we can just keep around an array describing whether a bound universe is covariant, invariant or irrelevant (CIC has no contravariant conversion rule). Printing is fairly obtuse and should be improved: when we print the CumulativityInfo we add marks to the universes of the instance: = for invariant, + for covariant and * for irrelevant. ie Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }. Print Foo. gives Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo { foo : Type@{i} -> Type@{j} } (* =i +j *k |= *) | ||
| * | [error] Replace msg_error by a proper exception. | 2018-02-09 | |
|/ | | | | | | | | | | The current error mechanism in the core part of Coq is 100% exception based; there was some confusion in the past as to whether raising and exception could be replace with `Feedback.msg_error`. As of today, this is not the case [due to some issues in the layer that generates error feedbacks in the STM] so all cases of `msg_error` must raise an exception of print at a different level [for now]. | ||
* | checker: cleanup projection unfolding | 2018-02-02 | |
| | | | | This just shares the unfold_projection between Closure and Reduction. | ||
* | checker: remove unused per-constant reduction flags. | 2018-02-02 | |
| | |||
* | [checker] Avoid relying on canonical names. | 2018-01-25 | |
| | | | | Fixes #5747: "make validate" fails with "bad recursive trees" | ||
* | [checker] Remove duplicated function | 2018-01-25 | |
| | |||
* | [checker] Better error message for bad recursive trees | 2018-01-25 | |
| | |||
* | fix space in coqchk error | 2018-01-24 | |
| | |||
* | Fix #6618: coqchk fails with "ill-typed term". | 2018-01-20 | |
| | | | | | | Primitive projections were not correctly unfolded, leading to failure of conversion checks in some cases. The kernel was strangely not affected by this bug, and it was probably a remnant of some vestigial code. | ||
* | Actually use the strategy information in the checker. | 2018-01-14 | |
| | |||
* | Store the conversion oracle in constant and inductive definitions. | 2018-01-14 | |
| | | | | | We also have to update the checker to deserialize this additional data, but it is not using it in type-checking yet. | ||
* | Add interfaces for checker and remove dead code. | 2018-01-10 | |
| | |||
* | Moving some universe substitution code out of the kernel. | 2017-12-30 | |
| | | | | | | This code was not used at all inside the kernel, it was related to universe unification that happens in the upper layer. It makes more sense to put it somewhere upper. | ||
* | [lib] Rename Profile to CProfile | 2017-12-09 | |
| | | | | | New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`. | ||
* | Merge PR #6277: Qualified import in coqchk | 2017-12-07 | |
|\ | |||
* \ | Merge PR #6303: Remove redundant Zcase from the checker. | 2017-12-07 | |
|\ \ | |||
* \ \ | Merge PR #6266: Safe unmarshalling in the checker | 2017-12-05 | |
|\ \ \ | |||
| | * | | Remove redundant Zcase from the checker. | 2017-12-02 | |
| |/ / |/| | | | | | | | | | | | | | | This was redundant with ZcaseT, the only difference lying in the use or not of fclosures for substerms. This code was removed from the kernel in commit f2f805ed, we finish the work in the checker now. | ||
| | * | Documenting the -Q flag of coqchk. | 2017-12-01 | |
| | | |