| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-25 | Merge PR #7325: Fix #7323: coqchk puts polymorphic univs of inductive in ↵ | Pierre-Marie Pédrot | |
| global env | |||
| 2018-05-24 | Merge PR #7177: Unifying names of "smart" combinators + adding combinators ↵ | Pierre-Marie Pédrot | |
| in CArray | |||
| 2018-05-24 | Fix #7323: coqchk puts polymorphic univs of inductive in global env | Gaëtan Gilbert | |
| 2018-05-24 | Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constants | Pierre-Marie Pédrot | |
| 2018-05-24 | Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant ↵ | Pierre-Marie Pédrot | |
| instances | |||
| 2018-05-23 | Moving Rtree.smart_map into Rtree.Smart.map. | Hugo Herbelin | |
| 2018-05-23 | Moving Option.smart_map to Option.Smart.map. | Hugo Herbelin | |
| 2018-05-23 | Collecting List.smart_* functions into a module List.Smart. | Hugo Herbelin | |
| 2018-05-23 | Collecting Array.smart_* functions into a module Array.Smart. | Hugo Herbelin | |
| 2018-05-13 | Infrastructure for ocamldebug on the checker | Gaëtan Gilbert | |
| 2018-04-23 | Fix #7327: coqchk subtyping of polymorphic constants | Gaëtan Gilbert | |
| 2018-04-20 | Fix #6798: coqchk ignores ugraph when comparing constant instances | Gaëtan Gilbert | |
| 2018-03-28 | [api] Deprecate a couple of aliases that we missed. | Emilio Jesus Gallego Arias | |
| 2018-03-09 | Merge PR #6800: [checker] Printer cleanup. | Maxime Dénès | |
| 2018-03-08 | Update checker to reflect rule on constructors of polymorphic inductive types | Matthieu Sozeau | |
| 2018-03-07 | [checker] Printer cleanup. | Emilio Jesus Gallego Arias | |
| Makes printing rules more explicit and should close #6799. | |||
| 2018-03-05 | Replace invalid tag @raises in ocamldoc comments with @raise | mrmr1993 | |
| 2018-03-05 | Merge PR #6855: Update headers following #6543. | Maxime Dénès | |
| 2018-02-28 | Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd) | Maxime Dénès | |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann | |
| 2018-02-21 | Merge PR #6740: Adding a sanity check on inductive variance subtyping. | Maxime Dénès | |
| 2018-02-19 | Merge PR #6728: Extrude monomorphic universe contexts from with Definition ↵ | Maxime Dénès | |
| constraints. | |||
| 2018-02-19 | Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵ | Maxime Dénès | |
| camlp4 | |||
| 2018-02-17 | Change references to CAMLP4 to CAMLP5 to be more accurate since we no | Jim Fehrle | |
| longer use camlp4. | |||
| 2018-02-16 | Extrude monomorphic universe contexts from with Definition constraints. | Pierre-Marie Pédrot | |
| We defer the computation of the universe quantification to the upper layer, outside of the kernel. | |||
| 2018-02-15 | Adding a sanity check on inductive variance subtyping. | Pierre-Marie Pédrot | |
| 2018-02-12 | Merge PR #6262: [error] Replace msg_error by a proper exception. | Maxime Dénès | |
| 2018-02-11 | dest_{prod,lam}: no Cast case (it's removed by whd) | Gaëtan Gilbert | |
| 2018-02-10 | Simplification: cumulativity information is variance information. | Gaëtan Gilbert | |
| 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 |= *) | |||
| 2018-02-09 | [error] Replace msg_error by a proper exception. | Emilio Jesus Gallego Arias | |
| 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]. | |||
| 2018-02-02 | checker: cleanup projection unfolding | Gaëtan Gilbert | |
| This just shares the unfold_projection between Closure and Reduction. | |||
| 2018-02-02 | checker: remove unused per-constant reduction flags. | Gaëtan Gilbert | |
| 2018-01-25 | [checker] Avoid relying on canonical names. | Maxime Dénès | |
| Fixes #5747: "make validate" fails with "bad recursive trees" | |||
| 2018-01-25 | [checker] Remove duplicated function | Maxime Dénès | |
| 2018-01-25 | [checker] Better error message for bad recursive trees | Maxime Dénès | |
| 2018-01-24 | fix space in coqchk error | Ralf Jung | |
| 2018-01-20 | Fix #6618: coqchk fails with "ill-typed term". | Pierre-Marie Pédrot | |
| 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. | |||
| 2018-01-14 | Actually use the strategy information in the checker. | Pierre-Marie Pédrot | |
| 2018-01-14 | Store the conversion oracle in constant and inductive definitions. | Pierre-Marie Pédrot | |
| We also have to update the checker to deserialize this additional data, but it is not using it in type-checking yet. | |||
| 2018-01-10 | Add interfaces for checker and remove dead code. | Maxime Dénès | |
| 2017-12-30 | Moving some universe substitution code out of the kernel. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-12-09 | [lib] Rename Profile to CProfile | Emilio Jesus Gallego Arias | |
| New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`. | |||
| 2017-12-07 | Merge PR #6277: Qualified import in coqchk | Maxime Dénès | |
| 2017-12-07 | Merge PR #6303: Remove redundant Zcase from the checker. | Maxime Dénès | |
| 2017-12-05 | Merge PR #6266: Safe unmarshalling in the checker | Maxime Dénès | |
| 2017-12-02 | Remove redundant Zcase from the checker. | Pierre-Marie Pédrot | |
| 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. | |||
| 2017-12-01 | Documenting the -Q flag of coqchk. | Pierre-Marie Pédrot | |
| 2017-11-29 | Forbid implicitly relative names in the checker. | Pierre-Marie Pédrot | |
| Before this patch, passing a mere identifier (without dots) to the checker would make it consider it as implicitly referring to a relative name. For instance, if passed "foo", it would have looked for "Bar.foo.vo" and "Qux.foo.vo" if those files were in the loadpath. This was quite ad-hoc. We remove this "feature" and require the user to always give either a filename or a fully qualified logical name. | |||
| 2017-11-29 | Mark the -I option in coqchk as deprecated and merge it with -Q. | Pierre-Marie Pédrot | |
| It is not doing the same thing as coqtop, and the corresponding coqtop semantics is irrelevant in the checker as the latter does not rely on ML code. | |||
| 2017-11-29 | Add a -Q option to coqchck. | Pierre-Marie Pédrot | |
| It has exactly the same effect as -R, because there is no such thing as implicit relativization for object files in coqchk, contrarily to what Require does in coqtop. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |