| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-12-11 | Merge PR #6368: [api] Remove yet another type alias. | Maxime Dénès | |
| 2017-12-11 | Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract. | Maxime Dénès | |
| 2017-12-09 | [api] Remove yet another type alias. | Emilio Jesus Gallego Arias | |
| 2017-12-07 | Merge PR #6290: Rename update to set, Fixes #6196 | Maxime Dénès | |
| 2017-12-06 | Fix #6323: stronger restrict universe context vs abstract. | Gaëtan Gilbert | |
| In the test we do [let X : Type@{i} := Set in ...] with Set abstracted. The constraint [Set < i] was lost in the abstract. Universes of a monomorphic reference [c] are considered to appear in the term [c]. | |||
| 2017-12-05 | Rename update to set, fixes #6196 | Paul Steckler | |
| 2017-12-01 | Cleanup API for registering universe binders. | Matthieu Sozeau | |
| - Regularly declared for for polymorphic constants - Declared globally for monomorphic constants. E.g mono@{i} := Type@{i} is printed as mono@{mono.i} := Type@{mono.i}. There can be a name clash if there's a module and a constant of the same name. It is detected and is an error if the constant is first but is not detected and the name for the constant not registered (??) if the constant comes second. Accept VarRef when registering universe binders Fix two problems found by Gaëtan where binders were not registered properly Simplify API substantially by not passing around a substructure of an already carrier-around structure in interpretation/declaration code of constants and proofs Fix an issue of the stronger restrict universe context + no evd leak This is uncovered by not having an evd leak in interp_definition, and the stronger restrict_universe_context. This patch could be backported to 8.7, it could also be triggered by the previous restrict_context I think. | |||
| 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-28 | Merge PR #1033: Universe binder improvements | Maxime Dénès | |
| 2017-11-28 | Merge PR #6248: [api] Remove aliases of `Evar.t` | 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 | Forbid repeated names in universe binders. | Gaëtan Gilbert | |
| 2017-11-25 | Universe binders survive sections, modules and compilation. | Gaëtan Gilbert | |
| 2017-11-25 | Allow local universe renaming in Print. | Gaëtan Gilbert | |
| 2017-11-25 | Make restrict_universe_context stronger. | Gaëtan Gilbert | |
| This fixes BZ#5717. Also add a test and fix a changed test. | |||
| 2017-11-24 | [lib] Generalize Control.timeout type. | Emilio Jesus Gallego Arias | |
| We also remove some internal implementation details from the mli file, there due historical reasons. | |||
| 2017-11-24 | Use Entries.constant_universes_entry more. | Gaëtan Gilbert | |
| This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean. | |||
| 2017-11-24 | restrict_universe_context: do not prune named universes. | Gaëtan Gilbert | |
| 2017-11-24 | Stop exposing UState.universe_context and its Evd wrapper. | Gaëtan Gilbert | |
| We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former). | |||
| 2017-11-24 | Separate checking univ_decls and obtaining universe binder names. | Gaëtan Gilbert | |
| 2017-11-24 | Use Maps and ids for universe binders | Gaëtan Gilbert | |
| Before sometimes there were lists and strings. | |||
| 2017-11-24 | Use type Universes.universe_binders. | Gaëtan Gilbert | |
| 2017-11-23 | Merge PR #6203: Fix universe polymorphic Program obligations. | Maxime Dénès | |
| 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-22 | Fix universe polymorphic Program obligations. | Matthieu Sozeau | |
| The universes of the obligations should all be non-algebraic as they might appear in instances of other obligations and instances only take non-algebraic universes as arguments. | |||
| 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-19 | [proof] Attempt to deprecate some V82 parts of the proof API. | Emilio Jesus Gallego Arias | |
| I followed what seems to be the intention of the code, with the original intention of remove the global imperative proof state. However, I fully fail to see why the new API is better than the old one. In fact the opposite seems the contrary. Still big parts of the "new proof engine" seem unfinished, and I'm afraid I am not the right person to know what direction things should take. | |||
| 2017-11-13 | [api] Insert miscellaneous API deprecation back to core. | Emilio Jesus Gallego Arias | |
| 2017-11-13 | [api] Another large deprecation, `Nameops` | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-11-06 | [api] Deprecate all legacy uses of Names in core. | Emilio Jesus Gallego Arias | |
| This will allow to merge back `Names` with `API.Names` | |||
| 2017-11-06 | Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core. | Maxime Dénès | |
| 2017-11-05 | Cosmetic changes in evar_map printer. | Hugo Herbelin | |
| 2017-11-05 | Preventively protect locally against failures of evar_map printer. | Hugo Herbelin | |
| It is not clear that this is really needed, but in case it happens, one will at least have a partial result available rather than an unexploitable global failure of the parser. | |||
| 2017-11-05 | Fixing a cause of failure of evar_map printer in debugger. | Hugo Herbelin | |
| Indeed, the debugger debugs coqtop but it is itself just an ocaml runtime extended with the coq printers. It does not know the environment, so, looking in the Global.env() for the printers can only fail. | |||
| 2017-11-04 | [api] Deprecate all legacy uses of Name.Id in core. | Emilio Jesus Gallego Arias | |
| This is a first step towards some of the solutions proposed in #6008. | |||
| 2017-11-03 | Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available. | Maxime Dénès | |
| 2017-11-03 | Merge PR #6047: A generic printer for ltac values | Maxime Dénès | |
| 2017-11-02 | Exporting ValTMap for use in Genintern. | Hugo Herbelin | |
| 2017-11-01 | Fix FIXME: use OCaml 4.02 generative functors when available. | Gaëtan Gilbert | |
| 4.02.3 has been the minimal OCaml version for a while now. | |||
| 2017-10-28 | Fixing #5401 (printing of patterns with bound anonymous variables). | Hugo Herbelin | |
| This fixes also #5731, #6035, #5364. | |||
| 2017-10-09 | Merge PR #1109: Handle some misc todos | Maxime Dénès | |
| 2017-10-06 | Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type ↵ | Maxime Dénès | |
| "_something") | |||
| 2017-10-05 | Merge PR #1102: On the detection of evars which "advanced" (and a fix to ↵ | Maxime Dénès | |
| BZ#5757) | |||
| 2017-10-05 | Merge PR #1101: Fixing an old proof engine bug in collecting evars with ↵ | Maxime Dénès | |
| cleared context. | |||
| 2017-10-05 | Fixing BZ#5769 (variable of type "_something" was named after invalid "_"). | Hugo Herbelin | |
| 2017-09-29 | Remove TODO comment (Evar.t is opaque) | Gaëtan Gilbert | |
| 2017-09-28 | Efficient computation of the names contained in an environment. | Pierre-Marie Pédrot | |
| 2017-09-28 | Efficient fresh name generation relying on sets. | Pierre-Marie Pédrot | |
| The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |