| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-12-27 | Merge PR #6439: [api] Also deprecate constructors of Decl_kinds. | Maxime Dénès | |
| 2017-12-27 | Merge PR #6289: Remove unused boolean from cl_context field of ↵ | Maxime Dénès | |
| Typeclasses.typeclass | |||
| 2017-12-23 | [api] Also deprecate constructors of Decl_kinds. | Emilio Jesus Gallego Arias | |
| Unfortunately OCaml doesn't deprecate the constructors of a type when the type alias is deprecated. In this case it means that we don't get rid of the kernel dependency unless we deprecate the constructors too. | |||
| 2017-12-18 | Merge PR #6436: Fix #5368: Canonical structure unification fails. | Maxime Dénès | |
| 2017-12-15 | Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml` | Maxime Dénès | |
| 2017-12-15 | Fix #5368: Canonical structure unification fails. | Pierre-Marie Pédrot | |
| Universe instances were lost during constructions of the canonical instance. | |||
| 2017-12-14 | Merge PR #6264: [kernel] Patch allowing to disable VM reduction. | Maxime Dénès | |
| 2017-12-14 | Merge PR #978: In printing, experimenting factorizing "match" clauses with ↵ | Maxime Dénès | |
| same right-hand side. | |||
| 2017-12-14 | Merge PR #6373: Further clean-up in Reductionops, removing unused lift ↵ | Maxime Dénès | |
| arguments. | |||
| 2017-12-14 | Merge PR #6169: Clean up/deprecated options | Maxime Dénès | |
| 2017-12-14 | Vm_compute: taking into account let-ins in parameters of constructors. | Hugo Herbelin | |
| 2017-12-14 | Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind. | Maxime Dénès | |
| 2017-12-13 | [econstr] Cleanup in `vernac/classes.ml`. | Emilio Jesus Gallego Arias | |
| We fix quite a few types, and perform some cleanup wrt to the evar_map, in particular we prefer to thread it now as otherwise it may become trickier to check when we are using the correct one. Thanks to @SkySkimmer for lots of comments and bug-finding. | |||
| 2017-12-12 | Decompiling pattern-matching: mini-removal dead code. | Hugo Herbelin | |
| 2017-12-12 | In printing, factorizing "match" clauses with same right-hand side. | Hugo Herbelin | |
| Moreover, when there are at least two clauses and the last most factorizable one is a disjunction with no variables, turn it into a catch-all clause. Adding options Unset Printing Allow Default Clause. to deactivate the second behavior, and Unset Printing Factorizable Match Patterns. to deactivate the first behavior (deactivating the first one deactivates also the second one). E.g. printing match x with Eq => 1 | _ => 0 end gives match x with | Eq => 1 | _ => 0 end or (with default clause deactivates): match x with | Eq => 1 | Lt | Gt => 0 end More to be done, e.g. reconstructing multiple patterns in Nat.eqb... | |||
| 2017-12-12 | Removing cumbersome location in multiple patterns. | Hugo Herbelin | |
| This is to have a better symmetry between CCases and GCases. | |||
| 2017-12-12 | Further clean-up in Reductionops, removing unused lift arguments. | Maxime Dénès | |
| This is a follow-up on 866b449c497933a3ab1185c194d8d33a86c432f2. | |||
| 2017-12-11 | [proof] Embed evar_map in RefinerError exception. | Emilio Jesus Gallego Arias | |
| The exception needs to carry aroud a pair of `env, sigma` so printing is correct. This gets rid of a few global calls, and it is IMO the right thing to do. While we are at it, we incorporate some fixes to a couple of additional printing functions missing the `env, sigma` pair. | |||
| 2017-12-11 | Remove deprecated option Tactic Compat Context. | Théo Zimmermann | |
| And some code simplification. | |||
| 2017-12-11 | Merge PR #6368: [api] Remove yet another type alias. | Maxime Dénès | |
| 2017-12-11 | Merge PR #6338: Remove up-to-conversion term matching | Maxime Dénès | |
| 2017-12-09 | [api] Remove yet another type alias. | Emilio Jesus Gallego Arias | |
| 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-09 | Remove up-to-conversion matching functions. | Pierre-Marie Pédrot | |
| They were not used anymore since the previous patches. | |||
| 2017-12-06 | Getting rid of the Update constructor in Reductionops. | Pierre-Marie Pédrot | |
| This was dead code, probably due to the fact it was once shared with the kernel stack type. | |||
| 2017-12-06 | Getting rid of the Shift constructor in Reductionops. | Pierre-Marie Pédrot | |
| It was actually not used. The only place generating one was easily writable without it. | |||
| 2017-12-02 | [kernel] Patch allowing to disable VM reduction. | Emilio Jesus Gallego Arias | |
| The patch has three parts: - Introduction of a configure flag `-bytecode-compiler (yes|no)` (due to static initialization this is a configure-time option) - Installing the hooks that register the VM with the pretyper and the kernel conditionally on the flag. - Replacing the normalization function in `Redexpr` by compute if the VM is disabled. We also rename `Coq_config.no_native_compiler` to `native_compiler` and `Flags.native_compiler` to `output_native_objects` [see #4607]. | |||
| 2017-12-01 | Proper nametab handling of global universe names | Matthieu Sozeau | |
| They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced | |||
| 2017-11-30 | Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ↵ | Maxime Dénès | |
| #3125) | |||
| 2017-11-30 | Remove unused boolean from cl_context field of Typeclasses.typeclass | Gaëtan Gilbert | |
| 2017-11-28 | Adding a variant get_truncation_family_of of get_sort_family_of. | Hugo Herbelin | |
| This function returns InProp or InSet for inductive types only when the inductive type has been explicitly truncated to Prop or (impredicative) Set. For instance, singleton inductive types and small (predicative) inductive types are not truncated and hence in Type. | |||
| 2017-11-28 | Moving non-recursive function sort_family_of out of the retype block of ↵ | Hugo Herbelin | |
| recursive functions. | |||
| 2017-11-28 | Merge PR #1033: Universe binder improvements | Maxime Dénès | |
| 2017-11-26 | [api] Remove aliases of `Evar.t` | Emilio Jesus Gallego Arias | |
| There don't really bring anything, we also correct some minor nits with the printing function. | |||
| 2017-11-25 | Fix interpretation of global universes in univdecl constraints. | Gaëtan Gilbert | |
| Also nicer error when the constraints are impossible. | |||
| 2017-11-24 | Use Maps and ids for universe binders | Gaëtan Gilbert | |
| Before sometimes there were lists and strings. | |||
| 2017-11-24 | Merge PR #486: Make some functions on terms more robust w.r.t new term ↵ | Maxime Dénès | |
| constructs. | |||
| 2017-11-23 | Make some functions on terms more robust w.r.t new term constructs. | Maxime Dénès | |
| Extending terms is notoriously difficult. We try to get more help from the compiler by making sure such an extension will trigger non exhaustive pattern matching warnings. | |||
| 2017-11-22 | [api] A few more minor deprecation notices. | Emilio Jesus Gallego Arias | |
| Note the problem with `create_evar_defs`. | |||
| 2017-11-22 | [api] Deprecate Term destructors, move to Constr | Emilio Jesus Gallego Arias | |
| We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`. | |||
| 2017-11-21 | [api] Miscellaneous consolidation + moves to engine. | Emilio Jesus Gallego Arias | |
| We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization. | |||
| 2017-11-20 | Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵ | Maxime Dénès | |
| unbound rel | |||
| 2017-11-15 | Fix #5761: cbv on undefined evars under binders produces unbound rel | Gaëtan Gilbert | |
| When an evar is undefined we need to substitute inside the evar instance. With help from @herbelin and @psteckler to identify the issue from a large test case. | |||
| 2017-11-13 | [api] Another large deprecation, `Nameops` | Emilio Jesus Gallego Arias | |
| 2017-11-13 | Merge PR #6098: [api] Move structures deprecated in the API to the core. | Maxime Dénès | |
| 2017-11-13 | Merge PR #6117: Fix printing anomaly in conv | Maxime Dénès | |
| 2017-11-13 | Merge PR #6065: [api] Deprecate all legacy uses of Names in core. | Maxime Dénès | |
| 2017-11-08 | Merge PR #922: New beta-iota compatibility refinements | Maxime Dénès | |
| 2017-11-08 | Fixing missing separator in an error message. | Hugo Herbelin | |
| The message is the "Conversion test raised an anomaly" one. | |||
| 2017-11-06 | [api] Move structures deprecated in the API to the core. | Emilio Jesus Gallego Arias | |
| We do up to `Term` which is the main bulk of the changes. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |