| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | 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-28 |
| |\ \ | |||
| | * | | [api] Remove aliases of `Evar.t` |  Emilio Jesus Gallego Arias | 2017-11-26 |
| | | | | | | | | | | | | | | | | There don't really bring anything, we also correct some minor nits with the printing function. | ||
| | | * | 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 | 2017-11-25 |
| | | | | | | | | | | | | | | | | | | | This fixes BZ#5717. Also add a test and fix a changed test. | ||
| * | | | [lib] Generalize Control.timeout type. | Emilio Jesus Gallego Arias | 2017-11-24 |
| |/ / | | | | | | | | | We also remove some internal implementation details from the mli file, there due historical reasons. | ||
| | * | Use Entries.constant_universes_entry more. | Gaëtan Gilbert | 2017-11-24 |
| | | | | | | | | | | | | | This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean. | ||
| | * | 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 | 2017-11-24 |
| | | | | | | | | | | | | | 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). | ||
| | * | 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 | 2017-11-24 |
| | | | | | | | | | Before sometimes there were lists and strings. | ||
| | * | Use type Universes.universe_binders. | Gaëtan Gilbert | 2017-11-24 |
| |/ | |||
| * | Merge PR #6203: Fix universe polymorphic Program obligations. | Maxime Dénès | 2017-11-23 |
| |\ | |||
| * | | [api] A few more minor deprecation notices. | Emilio Jesus Gallego Arias | 2017-11-22 |
| | | | | | | | | | Note the problem with `create_evar_defs`. | ||
| * | | [api] Deprecate Term destructors, move to Constr | Emilio Jesus Gallego Arias | 2017-11-22 |
| | | | | | | | | | | | | | | | 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`. | ||
| | * | Fix universe polymorphic Program obligations. |  Matthieu Sozeau | 2017-11-22 |
| | | | | | | | | | | | | | 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. | ||
| * | | [api] Miscellaneous consolidation + moves to engine. | Emilio Jesus Gallego Arias | 2017-11-21 |
| | | | | | | | | | | | | | 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. | ||
| * | | [proof] Attempt to deprecate some V82 parts of the proof API. | Emilio Jesus Gallego Arias | 2017-11-19 |
| |/ | | | | | | | | | | | | 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. | ||
| * | [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-13 |
| | | |||
| * | [api] Move structures deprecated in the API to the core. | Emilio Jesus Gallego Arias | 2017-11-06 |
| | | | | | We do up to `Term` which is the main bulk of the changes. | ||
| * | [api] Deprecate all legacy uses of Names in core. | Emilio Jesus Gallego Arias | 2017-11-06 |
| | | | | | This will allow to merge back `Names` with `API.Names` | ||
| * | Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core. | Maxime Dénès | 2017-11-06 |
| |\ | |||
| * | | Cosmetic changes in evar_map printer. |  Hugo Herbelin | 2017-11-05 |
| | | | |||
| * | | Preventively protect locally against failures of evar_map printer. | Hugo Herbelin | 2017-11-05 |
| | | | | | | | | | | | | | 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. | ||
| * | | Fixing a cause of failure of evar_map printer in debugger. | Hugo Herbelin | 2017-11-05 |
| | | | | | | | | | | | | | | | 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. | ||
| | * | [api] Deprecate all legacy uses of Name.Id in core. | Emilio Jesus Gallego Arias | 2017-11-04 |
| |/ | | | | This is a first step towards some of the solutions proposed in #6008. | ||
| * | 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-03 |
| |\ \ | |||
| | * | | Exporting ValTMap for use in Genintern. | Hugo Herbelin | 2017-11-02 |
| | | | | |||
| | | * | Fix FIXME: use OCaml 4.02 generative functors when available. | Gaëtan Gilbert | 2017-11-01 |
| | |/ | | | | | | | 4.02.3 has been the minimal OCaml version for a while now. | ||
| * / | Fixing #5401 (printing of patterns with bound anonymous variables). | Hugo Herbelin | 2017-10-28 |
| |/ | | | | This fixes also #5731, #6035, #5364. | ||
| * | Merge PR #1109: Handle some misc todos | Maxime Dénès | 2017-10-09 |
| |\ | |||
| * \ | Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type ↵ | Maxime Dénès | 2017-10-06 |
| |\ \ | | | | | | | | | | "_something") | ||
| * \ \ | Merge PR #1102: On the detection of evars which "advanced" (and a fix to ↵ | Maxime Dénès | 2017-10-05 |
| |\ \ \ | | | | | | | | | | | | | BZ#5757) | ||
| * \ \ \ | Merge PR #1101: Fixing an old proof engine bug in collecting evars with ↵ | Maxime Dénès | 2017-10-05 |
| |\ \ \ \ | | | | | | | | | | | | | | | | cleared context. | ||
| | | | * | | Fixing BZ#5769 (variable of type "_something" was named after invalid "_"). | Hugo Herbelin | 2017-10-05 |
| | | | | | | |||
| | | | | * | Remove TODO comment (Evar.t is opaque) | Gaëtan Gilbert | 2017-09-29 |
| | | | |/ | |||
| * | | | | 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 | 2017-09-28 |
| | |_|/ |/| | | | | | | | | | | | 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). | ||
| | | * | Moving setting of "cleared" evar flag directly in Evd.restrict. | Hugo Herbelin | 2017-09-27 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In particular, this fixes #5757 which used restrict_evar to refine the information on the source of an evar, and which should have set the "cleared" flag. Also renaming flag "restricted" since it is not only about "clear". I guess this is what we want in general, but I did not survey all uses of restrict_evar so, maybe, this should be refined further. | ||
| | | * | Fixing an old bug in collecting evars with cleared context. | Hugo Herbelin | 2017-09-27 |
| | |/ |/| | | | | | | | | | The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same. | ||
| | * | Fixing an old bug in collecting evars with cleared context. | Hugo Herbelin | 2017-09-27 |
| |/ | | | | | | The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same. | ||
| * | Merge PR #688: Binding universe constraints in Definition/Inductive/etc... | Maxime Dénès | 2017-09-26 |
| |\ | |||
| * \ | Merge PR #1036: Unify EConstr.t equality | Maxime Dénès | 2017-09-19 |
| |\ \ | |||
| | | * | Document UState.universe_context. | Gaëtan Gilbert | 2017-09-19 |
| | | | | |||
| | | * | Don't lose names in UState.universe_context. | Gaëtan Gilbert | 2017-09-19 |
| | | | | | | | | | | | | | | | | We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it. | ||
| | | * | proof_global: cleanup and comment close_proof |  Matthieu Sozeau | 2017-09-19 |
| | | | | | | | | | | | | | | | | | | | | | | evd: Move constrain_variables to an operation on UState Necessary to check universe declarations correctly for deferred proofs in particular. | ||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |