| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-10-16 | Refactoring proofview: make the definition of the logic monad polymorphic. | Arnaud Spiwack | |
| Makes the monad more flexible as it will be easier to add new components to the concrete state of the tactic monad. The Proofview module is also organised in a more abstract way with dedicated submodules to access various parts of the state or writer. | |||
| 2014-10-16 | Refresh to avoid algebraic universes on the right. | Matthieu Sozeau | |
| 2014-10-16 | Fix test-suite scripts. | Matthieu Sozeau | |
| 2014-10-16 | Bug fixed by Hugo. | Matthieu Sozeau | |
| 2014-10-16 | Grab Existential Variables: restore the goal order from v8.4. | Arnaud Spiwack | |
| Changes in the implementation details had unwittingly changed the order in which Grab Existential Variables displayed the goals. | |||
| 2014-10-16 | Proofview: cleanup: no more reference to Goal.goal. | Arnaud Spiwack | |
| 2014-10-16 | Put evars remaining after a tactic on the shelf. | Arnaud Spiwack | |
| Uses the new architecture which allows to keep track of all new evars. The [future_goals] are flushed at the end of the tactics, the [principal_future_goal] is ignored. | |||
| 2014-10-16 | Refine: proper scoping of the future goals. | Arnaud Spiwack | |
| In my first attempt I just dropped all future goals before starting a refinement. This was done for simplicity but is incorrect in general. In this version the future goals which are not introduced by the particular instance of refine are kept for future use. | |||
| 2014-10-16 | Goal: remove [advance] from the API. | Arnaud Spiwack | |
| Now [Goal] only contains a few helpers. | |||
| 2014-10-16 | Proofview: remove unused [refresh_sigma] compatibility primitive. | Arnaud Spiwack | |
| 2014-10-16 | Goal: remove some functions from the compatibility layer. | Arnaud Spiwack | |
| The rest will take more work. | |||
| 2014-10-16 | Goal: remove most of the API (make [Goal.goal] concrete). | Arnaud Spiwack | |
| We are left with the compatibility layer and a handful of primitives which require some thought to move. | |||
| 2014-10-16 | Make [Goal.goal] be exactly [Evar.t]. | Arnaud Spiwack | |
| First step in removing the [Goal] module whose code is now essentially legacy. Removes the cache attached to a goal, which was used to avoid unnecessary [nf_evar]. May have a performance cost, which is to be fixed later. | |||
| 2014-10-16 | Goal: remove dead code. | Arnaud Spiwack | |
| 2014-10-16 | Expose Proofview.Refine.with_type in the API. | Arnaud Spiwack | |
| 2014-10-16 | Proofview.Refine: remove the handle type, and simplify the API. | Arnaud Spiwack | |
| Now, usual function from Evarutil are used to define evars instead of the variants from Proofview.Refine. The [update] primitive which tried to patch the difference between pretyping functions and the refine primitive is now replaced by the identity function. | |||
| 2014-10-16 | Move the handling of the principal evar from refine to evd. | Arnaud Spiwack | |
| See previous commit for more discussion. Changed the name from "main" to "principal" because I find "main" overused, and because the name was only introduced yesterday anyway. | |||
| 2014-10-16 | Move the handling a new evars from the [Proofview.Refine] module to [Evd]. | Arnaud Spiwack | |
| That way, everything in the code of pretying is made "refine"-aware. Making the abstraction stonger and integration of pretyping with interactive proof more direct. It might create goals in a slightly different goal order in the (user level) refine tactic. Because now, the [update] primitive which used to infer an order from an [evar_map] now has the order fixed by the successive declaration with [Evarutil.new_evar] (and similar). It probably coincides, though. Following a suggestion by Hugo. | |||
| 2014-10-16 | Evd: a few comments to document the increasingly wide internal [evar_map] type. | Arnaud Spiwack | |
| 2014-10-16 | Evd: remove/update obsolete comments. | Arnaud Spiwack | |
| 2014-10-16 | Proofview.Refine: delay the marking of new evars as goals from [new_evar] to ↵ | Arnaud Spiwack | |
| [refine]. This makes [new_evar] closer to be a mere wrapper around [Evarutil.new_evars]. Will allow restructuring of the refinement interface. | |||
| 2014-10-16 | Proofview: small optimisation/simplification. | Arnaud Spiwack | |
| 2014-10-16 | ConstructiveEpsilon: simplify the before_witness type using non-uniform ↵ | Arnaud Spiwack | |
| parameters. | |||
| 2014-10-15 | Adding a timeout to bug #2447. | Pierre-Marie Pédrot | |
| 2014-10-15 | To stay closer to non-primitive projections, only unfold primitive | Matthieu Sozeau | |
| projections in cbv when delta _and_ beta flags are set. Add test-suite file for bug 3700 too. | |||
| 2014-10-15 | Make use of unfolded primitive projections when elaborating match on a | Matthieu Sozeau | |
| primitive record. | |||
| 2014-10-15 | Fix ill-typed debugging function | Matthieu Sozeau | |
| 2014-10-15 | Fix for bug #3618. | Matthieu Sozeau | |
| Fix typeclass resolution which was considering as subgoals of a tactic application unrelated pre-existing undefined evars. | |||
| 2014-10-15 | Remaining tactics of the Auto module were put in the monad. | Pierre-Marie Pédrot | |
| 2014-10-15 | Closed bug 3710. | Matthieu Sozeau | |
| 2014-10-15 | Bug 3692 is fixed. | Matthieu Sozeau | |
| 2014-10-15 | Bug 3628 is fixed. | Matthieu Sozeau | |
| 2014-10-15 | Fix test-suite files which failed due to usage of $(admit)$ which | Matthieu Sozeau | |
| now fails with Error: Already an existential evar of name Main | |||
| 2014-10-15 | Fix bug 3637. | Matthieu Sozeau | |
| 2014-10-15 | Reenable FO unification of primitive projections and their eta-expanded | Matthieu Sozeau | |
| forms in evarconv and unification, as well as fallback to first-order unification when eta for constructors fail. Update test-suite file 3484 to test for the FO case in evarconv as well. | |||
| 2014-10-15 | Fix test-suite file after moving back to using C as the name | Matthieu Sozeau | |
| of the record binder for Class C's projections. | |||
| 2014-10-15 | Modify the heuristic for unfolding lhs or rhs in evarconv, considering | Matthieu Sozeau | |
| folded primitive projections in applicative stacks in rhs as named, hence prefering to unfold the lhs in these cases. | |||
| 2014-10-15 | Implement a different strategy to expand primitive projections only when | Matthieu Sozeau | |
| required, i.e. in first-order unification cases where the head of the other side is a hole or the eta-expanded constant. | |||
| 2014-10-15 | Add an option to not print primitive projection parameters, which can | Matthieu Sozeau | |
| make printing exponentially slower. We would have to expand all projections at once before detyping to make this linear. | |||
| 2014-10-15 | Fix -async-proofs-always-delegate (close 3740) | Enrico Tassi | |
| 2014-10-14 | Fix ML paths (thanks Jean-Marc Notin for bisecting it) | Enrico Tassi | |
| 2014-10-14 | Revert "Move eta-expansion after delta reduction in kernel reduction. This ↵ | Matthieu Sozeau | |
| makes" This makes CatsInZFC explode by expanding constants unnecessarily. This reverts commit cf36105854c9a42960ee4139c6afdaa75ec8f31a. | |||
| 2014-10-14 | Oops, forgot a fix needed after the rebase. | Matthieu Sozeau | |
| 2014-10-14 | Fix bug #3698: stack overflow due to eta+canonical structures in | Matthieu Sozeau | |
| unification. | |||
| 2014-10-13 | Fix typo, thanks Mike Shulman for spotting it | Enrico Tassi | |
| 2014-10-13 | Fixing "change" and "fold" after convert_hyp/convert_concl moved to | Hugo Herbelin | |
| new proof engine in e824d4293. Because of the expansion made by "fold" and possibly by "change", checking the order of hypotheses is necessary in general in "reduce". Before, it was done by side-effect on reference "check", now it has to be explicit. To do for optimization: flag each of the red_expr conversion strategy according to whether they really need a check. Also renamed the e_reduce family to e_change to emphasize that some expansion can occur and that typing has to be rechecked. This fixes recent failure of CoLoR (and probably Ergo). | |||
| 2014-10-13 | Add support for deactivating type class inference from induction/destruct. | Hugo Herbelin | |
| 2014-10-13 | Adding a tactic which fails if one of the goals under focus is dependent in ↵ | Hugo Herbelin | |
| another one. | |||
| 2014-10-13 | Adding printers for ppproofview. | Hugo Herbelin | |
| 2014-10-13 | Naming main goal "Main" | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |