| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-01-22 | [CS] recognize applied primitive projections as keys (fix #9375) | Enrico Tassi | |
| 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 | |
| 2018-10-30 | Remove Environ.set_universes / Typing.enrich_env | Gaëtan Gilbert | |
| Made possible by the previous commit passing ~evars to check_hyps_inclusion. | |||
| 2018-10-30 | Check univ instances in Typing. | Gaëtan Gilbert | |
| 2018-10-30 | Reduction functions based on CClosure should take an env | Maxime Dénès | |
| This is because the env contains typing flags (such as sharing strategy). | |||
| 2018-10-30 | Avoid redefining reduction functions in fun_ind | Maxime Dénès | |
| We also stop passing dummy env and evar maps. | |||
| 2018-10-30 | Distinguish globalization and pretyping error on unbound variable | Maxime Dénès | |
| We can then avoid passing an empty env. | |||
| 2018-10-30 | Switch to using the obligation_evar flag instead of the evar source | Matthieu Sozeau | |
| for the determination of evars that can be turned into obligations. | |||
| 2018-10-29 | Fix for bug #8848 | Matthieu Sozeau | |
| 2018-10-29 | Merge PR #8667: [RFC] Vendoring of Camlp5 | Pierre-Marie Pédrot | |
| 2018-10-29 | Merge PR #8780: Cleanup comparing projections through their constants. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |