| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-04-23 | Merge PR #14075: New level of abstraction for streams with (non-canonical) ↵ | Pierre-Marie Pédrot | |
| location function Reviewed-by: ppedrot | |||
| 2021-04-23 | Merge PR #13965: [abbreviation] user syntax to set interp scope of argument | Pierre-Marie Pédrot | |
| Ack-by: JasonGross Reviewed-by: herbelin Reviewed-by: jashug Reviewed-by: jfehrle Reviewed-by: ppedrot | |||
| 2021-04-23 | Relying on the abstract notion of streams with location for parsing. | Hugo Herbelin | |
| We also get rid of ploc.ml, now useless, relying a priori on more robust code in lStream.ml for location reporting (see e.g. parse_parsable in grammar.ml). | |||
| 2021-04-18 | Merge PR #14112: Cleanup useless environment manipulation in Class declaration | coqbot-app[bot] | |
| Reviewed-by: ejgallego | |||
| 2021-04-14 | Cleanup useless environment manipulation in Class declaration | Gaëtan Gilbert | |
| 2021-04-14 | Remove remote counter system | Gaëtan Gilbert | |
| 2021-04-14 | Put async worker id in universe names | Gaëtan Gilbert | |
| This removes the need for the remote counter. | |||
| 2021-04-07 | [abbreviation] allow the user to set arguments scope | Enrico Tassi | |
| 2021-04-07 | cleanup: less exceptions, removal of try_interp_name_alias | Enrico Tassi | |
| 2021-04-06 | Missing dot in an error message. | Hugo Herbelin | |
| 2021-04-06 | One catch-all's missing a noncritical; another is now useless (see 7efaf86). | Hugo Herbelin | |
| 2021-04-06 | Uniformizing the "already exists" messages | Hugo Herbelin | |
| 2021-03-26 | [recordops] complete API rewrite; the module is now called [structures] | Enrico Tassi | |
| 2021-03-25 | Merge PR #13852: [vernac] Improve alpha-renaming in record projection types | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-03-24 | Mention label name in signature mismatch error when constant expected | Gaëtan Gilbert | |
| Fix #13987 | |||
| 2021-03-10 | Merge PR #13840: [notation] option to fine tune printing of literals | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Ack-by: jfehrle | |||
| 2021-03-09 | Add the source and target classes to the coercion table | Kazuhiko Sakaguchi | |
| `coe_source` and `coe_target` fields of type `cl_typ` have been added to `coe_info_typ` so that it allows querying the classes from a `GlobRef.t` of a coercion. The `coercion` record has also been replaced with `coe_info_typ`. | |||
| 2021-03-09 | Replace cl_index with cl_typ in coercionops.ml | Kazuhiko Sakaguchi | |
| The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been replaced with `cl_typ` and `ClTypMap` respectively. | |||
| 2021-03-06 | [vernac] Improve alpha-renaming in record projection types | Li-yao Xia | |
| 2021-03-04 | [notation] option to fine tune printing of literals | Enrico Tassi | |
| 2021-03-03 | [build] Split stdlib to it's own opam package. | Emilio Jesus Gallego Arias | |
| We introduce a new package structure for Coq: - `coq-core`: Coq's OCaml tools code and plugins - `coq-stdlib`: Coq's stdlib [.vo files] - `coq`: meta-package that pulls `coq-{core,stdlib}` This has several advantages, in particular it allows to install Coq without the stdlib which is useful in several scenarios, it also open the door towards a versioning of the stdlib at the package level. The main user-visible change is that Coq's ML development files now live in `$lib/coq-core`, for compatibility in the regular build we install a symlink and support both setups for a while. Note that plugin developers and even `coq_makefile` should actually rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust. There is a transient state where we actually look for both `$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support the non-ocamlfind plus custom variables. This will be much improved once #13617 is merged (which requires this PR first), then, we will introduce a `coq.boot` library so finally `coqdep`, `coqchk`, etc... can share the same path setup code. IMHO the plan should work fine. | |||
| 2021-02-28 | Merge PR #13853: Delay the dynamic linking of native-code libraries until ↵ | Pierre-Marie Pédrot | |
| native_compute is called. Ack-by: ejgallego Reviewed-by: ppedrot | |||
| 2021-02-26 | Merge PR #13869: Use make_case_or_project in auto_ind_decl | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2021-02-26 | Delay the dynamic linking of native-code libraries until native_compute is ↵ | Guillaume Melquiond | |
| called (fix #13849). The libraries are eventually linked in native_norm and native_conv_gen, just before mk_norm_code and mk_conv_code are called. This commit also renames call_linker as execute_library to better reflect its role. It also makes link_library independent from it, since their error handling are completely opposite. | |||
| 2021-02-25 | [proof using] Remove duplicate code, refactor. | Emilio Jesus Gallego Arias | |
| PR #13183 introduced quite a bit of duplicate code, we refactor it and expose less internals on the way. That should make the API more robust. | |||
| 2021-02-24 | Infrastructure for fine-grained debug flags | Maxime Dénès | |
| 2021-02-17 | Use make_case_or_project in auto_ind_decl | Gaëtan Gilbert | |
| Towards #5154 (but insufficient) | |||
| 2021-02-17 | Reduce imperative arrays in build_beq_scheme + reindent | Gaëtan Gilbert | |
| 2021-02-17 | Merge PR #13734: Fix #13732: Implicit Type vs universes | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2021-02-11 | Merge PR #13844: [vernac] pass the loc of the whole command to the interp ↵ | coqbot-app[bot] | |
| function Reviewed-by: ejgallego | |||
| 2021-02-11 | [vernac] pass the loc of the whole command to the interp function | Enrico Tassi | |
| 2021-02-04 | Remove deprecated -sprop-cumulative command line argument | Gaëtan Gilbert | |
| Deprecated since #12034 (8.12) | |||
| 2021-01-28 | vernac/declaremods: make object collection tail-recursive | Gabriel Scherer | |
| This patch is trying to upstream a jsCoq patch that was written to solve Stack Overflow issues: https://github.com/jscoq/jscoq/blob/v8.12/etc/patches/cps.patch It turns List.fold_right in vernac/declaremods into List.fold_left on a reversed lit. | |||
| 2021-01-28 | Merge PR #13763: Remove the SearchHead command (deprecated in 8.12) | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 | |||
| 2021-01-28 | Merge PR #13790: [vernac] Check that no proofs do remain open at ↵ | coqbot-app[bot] | |
| section/module closing time Reviewed-by: SkySkimmer | |||
| 2021-01-27 | [vernac] move vernac_classifier to vernac | Enrico Tassi | |
| 2021-01-26 | [vernac] Check that no proofs do remain open at section/module closing time | Emilio Jesus Gallego Arias | |
| Fixes #13755 . | |||
| 2021-01-26 | Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12) | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 | |||
| 2021-01-25 | Remove the SearchHead command | Jim Fehrle | |
| 2021-01-25 | Remove the Hide Obligations flag | Jim Fehrle | |
| 2021-01-20 | Merge PR #13744: Make sure "Print Module" write a dot at the end of ↵ | coqbot-app[bot] | |
| inductive definitions. Reviewed-by: SkySkimmer | |||
| 2021-01-18 | Support locality attributes for Hint Rewrite (including export) | Gaëtan Gilbert | |
| We deprecate unspecified locality as was done for Hint. Close #13724 | |||
| 2021-01-14 | Merge PR #13378: Add support for high resolution timeout functions | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot | |||
| 2021-01-13 | Make sure "Print Module" write a dot at the end of inductive definitions. | Guillaume Melquiond | |
| 2021-01-11 | Do not declare a global universe object when the universe set is empty. | Pierre-Marie Pédrot | |
| 2021-01-11 | Fix #13732: Implicit Type vs universes | Gaëtan Gilbert | |
| This returns to the previous behaviour of Implicit Type forgetting universes. `Implicit Type T : Type@{u}.` may be confusing as it is equivalent to `: Type`, but until we have a better idea of what to do with anonymous types I see no other solution, especially in the short term to fix the bug. | |||
| 2021-01-09 | Merge PR #13299: Remember universe instances of constants in notations | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer Reviewed-by: herbelin | |||
| 2021-01-07 | Merge PR #13718: Move printing and sorting out of AcyclicGraph | coqbot-app[bot] | |
| Reviewed-by: SkySkimmer | |||
| 2021-01-06 | Further pushing up the printing and sorting of universes. | Pierre-Marie Pédrot | |
| We expose the representation function in UGraph and change the printer signature to work over the representation instead of the abstract type. Similarly, the topological sorting algorithm is moved to Vernacentries. It is now even simpler. | |||
| 2021-01-04 | Remember universe instances of constants in notations | Jasper Hugunin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |