| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-06-04 | Proof_global: pass only 1 pstate when we don't want the proof stack | Gaëtan Gilbert | |
| Typically instead of [start_proof : ontop:Proof_global.t option -> bla -> Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and the pstate is pushed on the stack by a caller around the vernacentries/mlg level. Naming can be a bit awkward, hopefully it can be improved (maybe in a followup PR). We can see some patterns appear waiting for nicer combinators, eg in mlg we often only want to work with the current proof, not the stack. Behaviour should be similar modulo bugs, let's see what CI says. | |||
| 2019-05-27 | mind_kelim is the highest allowed sort instead of a list | Gaëtan Gilbert | |
| 2019-05-27 | Merge PR #10237: Fix some incorrect uses of proof-local environment | Pierre-Marie Pédrot | |
| Reviewed-by: gares Reviewed-by: ppedrot | |||
| 2019-05-24 | Stop using pstate in global print queries | Gaëtan Gilbert | |
| Using pstate makes no sense for printing global stuff | |||
| 2019-05-24 | Fixing typos | JPR | |
| 2019-05-23 | Fixing typos - Part 3 | JPR | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |