| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-05-21 | Merge PR #10174: Further cleanup of the side-effect machinery | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Reviewed-by: gares Reviewed-by: maximedenes | |||
| 2019-05-21 | Merge PR #10144: Fix #9919: conversion functions are non-linear | Hugo Herbelin | |
| Ack-by: herbelin Reviewed-by: maximedenes Ack-by: ppedrot | |||
| 2019-05-19 | Merge the definition of constants and private constants in the API. | Pierre-Marie Pédrot | |
| 2019-05-15 | Merge PR #10151: Clean up the API for side-effects | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Ack-by: gares | |||
| 2019-05-15 | Simplify the private constant API. | Pierre-Marie Pédrot | |
| We ungroup the rewrite scheme-defined constants, while only exporting a function to turn the last added constant into a private constant. | |||
| 2019-05-14 | Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2 | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Reviewed-by: ppedrot | |||
| 2019-05-14 | Remove the sidecond_first flag of apply-related tactics. | Pierre-Marie Pédrot | |
| This was dead code. | |||
| 2019-05-14 | Remove the elimrename field from Tactics.eliminator. | Pierre-Marie Pédrot | |
| This is actually dead code, we never observe it. | |||
| 2019-05-14 | Code factorization in elim tactics. | Pierre-Marie Pédrot | |
| This is just moving code around, so it should not change the semantics. | |||
| 2019-05-14 | Allow run_tactic to return a value, remove hack from ltac2 | Gaëtan Gilbert | |
| 2019-05-13 | Merge PR #9887: [api] Remove 8.10 deprecations. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-05-11 | Actually use the conversion locality flag. | Pierre-Marie Pédrot | |
| Fixes #9919. | |||
| 2019-05-11 | Introducing a local flag to hypothesis conversion function. | Pierre-Marie Pédrot | |
| If the reduction function is known not to depend on the named context, then we can perform it in parallel on the various variables. | |||
| 2019-05-11 | Abstract the Tactic.e_change_hyps function over the reduction function. | Pierre-Marie Pédrot | |
| 2019-05-10 | Take advantage of the ordering / conversion check split. | Pierre-Marie Pédrot | |
| 2019-05-10 | Split the hypothesis conversion check in a conversion + ordering check. | Pierre-Marie Pédrot | |
| 2019-05-10 | Make the check flag of conversion functions mandatory. | Pierre-Marie Pédrot | |
| The current situation is a mess, some functions set it by default, but other no. Making it mandatory ensures that the expected value is the correct one. | |||
| 2019-05-10 | Logic.convert_hyp now takes an environment as an argument. | Pierre-Marie Pédrot | |
| This prevents having to call global functions, for no good reason. We also seize the opportunity to name the check argument. | |||
| 2019-05-10 | [api] Remove 8.10 deprecations. | Emilio Jesus Gallego Arias | |
| Some of them are significant so presumably it will take a bit of effort to fix overlays. I left out the removal of `nf_enter` for now as MTac2 needs some serious porting in order to avoid it. | |||
| 2019-05-05 | Merge PR #10059: Fixing bugs introduced in change_no_check | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-05-04 | Merge PR #9996: Fix #5752: `Hint Mode` ignored for type classes that appear ↵ | Pierre-Marie Pédrot | |
| as assumptions Ack-by: RalfJung Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: maximedenes Reviewed-by: ppedrot Ack-by: robbertkrebbers | |||
| 2019-05-03 | Tactics: fixing "change_no_check in". | Hugo Herbelin | |
| (Merge of the initial version with #9983 was broken) | |||
| 2019-05-03 | Fix #9994: `revert dependent` is extremely slow. | Pierre-Marie Pédrot | |
| We add a fast path when generalizing over variables. | |||
| 2019-05-02 | Remove outdated comment | Maxime Dénès | |
| 2019-05-02 | Fix #5752: `Hint Mode` ignored for type classes that appear as assumptions | Maxime Dénès | |
| The creation of the local hint db now inherits the union of the modes from the dbs passed to `typeclasses eauto`. We could probably go further and define in a more systematic way the metadata that should be inherited. A lot of this code could also be cleaned-up by defining the merge of databases, so that the search code is parametrized by just one db (the merge of the input ones). | |||
| 2019-05-02 | Use GlobRef.Map.t in hint databases | Maxime Dénès | |
| 2019-05-02 | Document typeclasses_eauto | Maxime Dénès | |
| 2019-04-29 | Exposing a change_no_check tactic. | Hugo Herbelin | |
| 2019-04-24 | Allocate only one evar when applying a group of conversion tactics. | Pierre-Marie Pédrot | |
| 2019-04-24 | Code factorization in conversion tactics. | Pierre-Marie Pédrot | |
| 2019-04-23 | Deprecate the *_no_check variants of conversion tactics. | Pierre-Marie Pédrot | |
| 2019-04-20 | Merge PR #9836: [schemes] Don't re-declare scheme side-effects that are ↵ | Enrico Tassi | |
| already there. Reviewed-by: gares | |||
| 2019-04-10 | Remove calls to global env in Inductiveops | Maxime Dénès | |
| 2019-04-10 | Remove calls to Global.env in Patternops | Maxime Dénès | |
| 2019-04-10 | Functionalize env in type classes | Maxime Dénès | |
| I had to reorganize the code a bit. The Context command moved to comAssumption, as it is not so related to type classes. We were able to remove a few hooks on the way. | |||
| 2019-04-10 | Remove one call to Global.env in Detyping | Maxime Dénès | |
| One other call still remains, but will require to refactor some section-handling code. | |||
| 2019-04-10 | Remove calls to global env from indrec | Maxime Dénès | |
| 2019-04-02 | Merge PR #8984: Declare initial hint databases in prelude | Pierre-Marie Pédrot | |
| Ack-by: JasonGross Reviewed-by: ppedrot | |||
| 2019-04-02 | Merge PR #9659: Fix #9652: rewrite fails to detect lack of progress | Emilio Jesus Gallego Arias | |
| Ack-by: SkySkimmer Reviewed-by: ejgallego Reviewed-by: ppedrot | |||
| 2019-03-31 | Merge PR #9841: Remove some [let foo = foo] in eqschemes | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-03-27 | [geninterp] Track polymorphic status in tactic interpretation. | Emilio Jesus Gallego Arias | |
| 2019-03-27 | [tactic] Adapt tactic layer to removal of imperative proof state. | Emilio Jesus Gallego Arias | |
| State in `Proof_global` was mostly used for debugging, so not a big change. | |||
| 2019-03-27 | Remove some [let foo = foo] in eqschemes | Gaëtan Gilbert | |
| 2019-03-26 | [kernel] Don't re-declare scheme side-effects that are already there. | Emilio Jesus Gallego Arias | |
| This is an experimental PR as I am not sure I can follow the reasoning in e1ba72037191b1d4be9de8a0a8fc1faa24eeb12c Note that in safe_typing we avoid re-declaring effects twice. This removes a huge number of redeclaration of schemes side-effects that in fact are already generated such as `eq_ind`. Anyways we should deprecate the declaration of Schemes on-the-fly, I don't see the point honestly; just make sure your theory has the right ones. Well, going to a more eager declaration scheme could be costly in terms of size, so OMMV. TODO: only declare side-effects if the scheme is generated on-the-fly, add a parameter to the declaration function. | |||
| 2019-03-26 | Declare initial hint databases in prelude | Maxime Dénès | |
| Previously, they were hard-wired in the ML code. | |||
| 2019-03-25 | Fix #9652: rewrite fails to detect lack of progress | Gaëtan Gilbert | |
| 2019-03-20 | Stop accessing proof env via Pfedit in printers | Maxime Dénès | |
| This should make https://github.com/coq/coq/pull/9129 easier. | |||
| 2019-03-14 | Add relevance marks on binders. | Gaëtan Gilbert | |
| Kernel should be mostly correct, higher levels do random stuff at times. | |||
| 2019-03-14 | Add a non-cumulative impredicative universe SProp. | Gaëtan Gilbert | |
| Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged. | |||
| 2019-03-14 | Make Sorts.t private | Gaëtan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |