| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-02-05 | Merge PR #9397: Simplify code for Recordops.cs_pattern_of_constr | Matthieu Sozeau | |
| Ack-by: SkySkimmer Reviewed-by: gares Ack-by: mattam82 | |||
| 2019-02-04 | Merge PR #6914: Primitive integers | Pierre-Marie Pédrot | |
| Ack-by: JasonGross Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Ack-by: maximedenes Ack-by: ppedrot | |||
| 2019-02-04 | Merge PR #9144: Fixes #4633: clearer message unknown existential | Pierre-Marie Pédrot | |
| Ack-by: herbelin Reviewed-by: ppedrot | |||
| 2019-02-04 | Primitive integers | Maxime Dénès | |
| This work makes it possible to take advantage of a compact representation for integers in the entire system, as opposed to only in some reduction machines. It is useful for heavily computational applications, where even constructing terms is not possible without such a representation. Concretely, it replaces part of the retroknowledge machinery with a primitive construction for integers in terms, and introduces a kind of FFI which maps constants to operators (on integers). Properties of these operators are expressed as explicit axioms, whereas they were hidden in the retroknowledge-based approach. This has been presented at the Coq workshop and some Coq Working Groups, and has been used by various groups for STM trace checking, computational analysis, etc. Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr> Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr> | |||
| 2019-02-04 | Merge PR #9368: Discard argument names of section variables on section close | Pierre-Marie Pédrot | |
| Reviewed-by: gares Reviewed-by: ppedrot | |||
| 2019-01-24 | Simplify code for Recordops.cs_pattern_of_constr | Gaëtan Gilbert | |
| This has different behaviour if called on an applied Rel, not sure if that ever happens. | |||
| 2019-01-22 | [CS] recognize applied primitive projections as keys (fix #9375) | Enrico Tassi | |
| 2019-01-20 | Discard argument names of section variables on section close | Jasper Hugunin | |
| 2019-01-06 | Fixes #4633: more explicit error message when referring to a generated evar. | Hugo Herbelin | |
| 2019-01-06 | Renaming pr_evar_suggested_name into -> evar_suggested_name. | Hugo Herbelin | |
| Since it returns an Id.t and not a Pp.t. | |||
| 2018-12-21 | Fix #9240: Register for IDProp causes anomaly when non constant | Gaëtan Gilbert | |
| 2018-12-18 | [arguments] cleanup | Enrico Tassi | |
| 2018-12-12 | Higher-level libobject API for objects with fixed scopes | Maxime Dénès | |
| 2018-12-12 | Merge PR #8974: Fix mod_subst wrt universe polymorphism | Maxime Dénès | |
| 2018-12-12 | Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix ↵ | Maxime Dénès | |
| comments. | |||
| 2018-12-09 | [doc] Enable Warning 50 [incorrect doc comment] and fix comments. | Emilio Jesus Gallego Arias | |
| This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :) | |||
| 2018-12-06 | Revise API for global universes. | Gaëtan Gilbert | |
| Rename Univ.Level.{Qualid -> UGlobal}, remove Univ.Level.Id. Remove the ability to split the argument of `Univ.Level.Level` into a dirpath*int pair (except by going through string hacks like detyping/pretyping(/funind) does). Id.of_string_soft to turn unnamed universes into qualid is pushed up to detyping. (TODO some followup PR clean up more) This makes it pointless to have an opaque type for ints in Univ.Level: it would only be used as argument to Univ.Level.UGlobal.make, ie ~~~ open Univ.Level let x = UGlobal.make dp (Id.make n) (* vs *) let x = UGlobal.make dp n ~~~ Remaining places which create levels from ints are various hacks (eg the dummy in inductive.ml, the Type.n universes in ugraph sort_universes) and univgen. UnivGen does have an opaque type for ints used as univ ids since they get manipulated by the stm. NB: build breaks due to ocamldep issue if UGlobal is named Global instead. | |||
| 2018-12-06 | Fix race condition triggered by fresh universe generation | Maxime Dénès | |
| Remote counters were trying to build universe levels (as opposed to simple integers), but did not have access to the right dirpath at construction time. We fix it by constructing the level only at use time, and we introduce some abstractions for qualified and unqualified level names. | |||
| 2018-12-05 | Fix mod_subst wrt universe polymorphism | Gaëtan Gilbert | |
| 2018-11-28 | Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a class | Matthieu Sozeau | |
| 2018-11-28 | [options] New helper for creation of boolean options plus reference. | Emilio Jesus Gallego Arias | |
| This makes setting the option outside of the synchronized summary impossible. | |||
| 2018-11-27 | Merge PR #9046: Goptions.declare_* functions return unit instead of a ↵ | Emilio Jesus Gallego Arias | |
| write_function | |||
| 2018-11-27 | Merge PR #7696: Remove some univ_flexible_alg from cases | Pierre-Marie Pédrot | |
| 2018-11-27 | Merge PR #8255: Fast typing of application nodes | Maxime Dénès | |
| 2018-11-27 | [Typeclasses] Warn when RHS of `:>` is not a class | Vincent Laporte | |
| This introduces the warning “not-a-class” in the “typeclasses” category. | |||
| 2018-11-24 | Merge PR #8929: Fix fixpoint related lifting in open recursors + related ↵ | Pierre-Marie Pédrot | |
| cleanups | |||
| 2018-11-23 | s/let _ =/let () =/ in some places (mostly goptions related) | Gaëtan Gilbert | |
| 2018-11-21 | Make initial evar map argument to check_evars_are_solved optional. | Gaëtan Gilbert | |
| (same for solve_remaining_evars) This is the standard way to use these functions, with 1 exception in Unification. | |||
| 2018-11-20 | Use a closure for the domain argument of FProd. | Pierre-Marie Pédrot | |
| The use of a term is not needed for the fast typing algorithm of the application case, so this tweak brings the best of both worlds. | |||
| 2018-11-20 | Do not wrap FProd return types in a closure. | Pierre-Marie Pédrot | |
| There is little point to this as the type is dependent on an open value and is never computed further. | |||
| 2018-11-19 | Rename TranspState into TransparentState. | Pierre-Marie Pédrot | |
| 2018-11-19 | Proper record type and accessors for transparent states. | Pierre-Marie Pédrot | |
| This is documented in dev/doc/changes.md. | |||
| 2018-11-19 | Move transparent_state to its own module. | Pierre-Marie Pédrot | |
| 2018-11-16 | Merge PR #8779: Remove the implicit tactic feature following #7229. | Matthieu Sozeau | |
| 2018-11-16 | Termops.iter_constr_with_full_binders = EConstr.iter_with_full_binders | Gaëtan Gilbert | |
| 2018-11-16 | Remove some univ_flexible_alg from cases | Gaëtan Gilbert | |
| There are a couple left which seem OK. | |||
| 2018-11-16 | No Projection.constant in projection <-> constant declaration | Gaëtan Gilbert | |
| Enabled by previous commit about Heads. | |||
| 2018-11-16 | Heads: simplify using that projections are always rigid | Gaëtan Gilbert | |
| This avoids using Projection.constant in kind_of_head, which then allows compute_head to not check whether the constant is a compatibility definition (as in that case its body is [fun ... => x.(p)]). Thus Heads stops caring about the compatibility projection system. | |||
| 2018-11-16 | Remove the implicit tactic feature following #7229. | Pierre-Marie Pédrot | |
| 2018-11-12 | Fix #8908: incorrect refresh of algebraic universes. | Gaëtan Gilbert | |
| 2018-11-09 | Adding universe names to polymorphic entry instances. | Pierre-Marie Pédrot | |
| 2018-11-06 | Move debug term printer to kernel | Maxime Dénès | |
| 2018-11-05 | Merge PR #7952: Fix an algorithmic issue in the vernac guardedness checker. | Gaëtan Gilbert | |
| 2018-11-05 | Merge PR #8896: Expose Typing.judge_of_apply | Pierre-Marie Pédrot | |
| 2018-11-05 | Merge PR #8866: Check universe instances in Typing | Pierre-Marie Pédrot | |
| 2018-11-05 | Merge PR #8842: Towards seeing Global purely as a wrapper on top of kernel ↵ | Maxime Dénès | |
| functions | |||
| 2018-11-03 | Merge PR #8852: Use the obligation evar flag | Pierre-Marie Pédrot | |
| 2018-11-02 | Expose Typing.judge_of_apply | Gaëtan Gilbert | |
| This can be useful to avoid [Typing.type_of (App (f,args))] when working with universe polymorphism. | |||
| 2018-10-31 | Renaming is_template_polymorphic -> is_template_polymorphic_ind. | Hugo Herbelin | |
| This emphasizes that it works only on inductive types. Also, the name is_template_polymorphic will be reused for a more general version. | |||
| 2018-10-31 | Merge PR #8864: Avoid passing empty environments | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |