| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-05-16 | Decent error message when a constant is not found | Enrico Tassi | |
| 2014-05-16 | Fix unification of non-unfoldable primitive projections in evarconv. | Matthieu Sozeau | |
| 2014-05-16 | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot | |
| "coretactics.ml4" file. | |||
| 2014-05-16 | Slightly better printer for native ML tactics, in order to disambiguate | Pierre-Marie Pédrot | |
| them. | |||
| 2014-05-16 | Tactics defined through TACTIC EXTEND that are only defined as a string do | Pierre-Marie Pédrot | |
| not create grammar and printing rules anymore, they define Ltac entries in the module that declares them instead. | |||
| 2014-05-16 | Another try at close_proof that should behave better w.r.t. exception handling. | Matthieu Sozeau | |
| 2014-05-15 | heads: avoid forcing opaque proofs | Enrico Tassi | |
| 2014-05-15 | poly: remove unused attribute to STM nodes and vernac classificaiton | Enrico Tassi | |
| 2014-05-15 | Polymorphic Lemmas are like Defined ones for STM | Enrico Tassi | |
| 2014-05-15 | Future: better error message | Enrico Tassi | |
| 2014-05-13 | Fix the behaviour of ML tactic notations w.r.t. Imports by making them | Pierre-Marie Pédrot | |
| substitutive. | |||
| 2014-05-13 | Test-suite for bug #3259. | Pierre-Marie Pédrot | |
| 2014-05-13 | Rewritten the sorting algorithm for universes with a better complexity. | Pierre-Marie Pédrot | |
| This should be now linear instead of the cubic Bellman-Ford algorithm. The new algorithm assumes that the universe graph is a DAG if we remove the {Le, Eq}-cycles, which is the case when the graph is consistent. Luckily we only use the sorting algorithm on such consistent graphs, in the Print Sorted Universes command. | |||
| 2014-05-12 | Update various polyproj bugs w.r.t. latest trunk | Jason Gross | |
| 2014-05-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot | |
| corresponding Declare ML Module command. This changes essentially two things: 1. ML plugins are forced to use the DECLARE PLUGIN statement before any TACTIC EXTEND statement. The plugin name must be exactly the string passed to the Declare ML Module command. 2. ML tactics are only made available after the Coq module that does the corresponding Declare ML Module is imported. This may break a few things, as it already broke quite some uses of omega in the stdlib. | |||
| 2014-05-12 | Moving the ML tactic extension mechanism to a Libobject-based one. | Pierre-Marie Pédrot | |
| 2014-05-12 | Plugin names must be declared in the header of .ml4 file, be they static or | Pierre-Marie Pédrot | |
| dynamic. This is done with the "DECLARE PLUGIN \"name\"" macro. | |||
| 2014-05-12 | Adding the possibility for ML modules to declare functions to be called at | Pierre-Marie Pédrot | |
| caching time, i.e. when the Declare ML Module command is evaluated. This can be used by both static and dynamic plugins. | |||
| 2014-05-12 | Fixing the undocumented -dumpgraphbox option of coqdep. | Pierre-Marie Pédrot | |
| 2014-05-11 | Using Maps to handle imports in Safe_typing. The order is irrelevant indeed, | Pierre-Marie Pédrot | |
| and the lookup operation proved to be costly when dealing with big libraries. | |||
| 2014-05-11 | Eliminating a potentially quadratic behaviour in Require, by using maps | Pierre-Marie Pédrot | |
| instead of lists to test if a library has already been encountered. | |||
| 2014-05-10 | Add appropriate Fail(s) to opened bugs | Jason Gross | |
| The contract is that a file in bugs/opened should not raise errors if the bug is still open. Some of them fail for different reasons than they used to; I'm not sure what to do about these. | |||
| 2014-05-10 | Move opened bugs to bugs/opened | Jason Gross | |
| 2014-05-10 | Add more regression tests for univ poly/prim proj | Jason Gross | |
| hese regression tests are aggregated from the various bugs I (and others) have reported on https://github.com/HoTT/coq/issues relating to universe polymorphism, primitive projections, and eta for records. These are the tests that trunk currently fails. I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the number of the issue in GitHub), but I couldn't think of a better one. | |||
| 2014-05-09 | Code cleaning & factorizing functions in Equality. | Pierre-Marie Pédrot | |
| 2014-05-09 | Update and start testing rewrite-in-type code. | Matthieu Sozeau | |
| 2014-05-09 | More documentation of new features in CHANGE. | Pierre-Marie Pédrot | |
| 2014-05-09 | Refresh universes for Ltac's type_of, as the term can be used anywhere, | Matthieu Sozeau | |
| fixing two opened bugs from HoTT/coq. | |||
| 2014-05-09 | Merge branch 'working-polyproj-tests' of https://github.com/JasonGross/coq ↵ | Matthieu Sozeau | |
| into JasonGross-working-polyproj-tests | |||
| 2014-05-09 | Fix second-order matching to properly check that the predicate found by | Matthieu Sozeau | |
| abstraction has the right type. Fixes bug# 3306. Add test-suite files for bugs 3305 and 3306. | |||
| 2014-05-09 | Restore implicit arguments of irreflexivity (fixes bug #3305). | Matthieu Sozeau | |
| 2014-05-09 | Reuse universe level substitutions for template polymorphism, fixing performance | Matthieu Sozeau | |
| problem with hashconsing at the same time. This fixes bug# 3302. | |||
| 2014-05-08 | Encapsulating some clausenv uses. This simplifies the control flow of some | Pierre-Marie Pédrot | |
| tactics. | |||
| 2014-05-08 | Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic." | Hugo Herbelin | |
| (made push command with wrong local ref; leaving control to Matthieu on new revert) This reverts commit b797ba85b7b0f82d66af5629ccf6f75d90dda99a. | |||
| 2014-05-08 | Avoid "revert" to retype-check the goal, and move it to a "new" tactic. | Hugo Herbelin | |
| 2014-05-08 | Typo reference manual | Hugo Herbelin | |
| 2014-05-08 | Isolating a function "make_abstraction", new name of "letin_abstract", | Hugo Herbelin | |
| which compute an abstraction of the goal over a term or a pattern. | |||
| 2014-05-08 | Simplification and improvement of "subst x" in such a way that it | Hugo Herbelin | |
| works in the presence of local definitions referring to x and dependent in other hyps or concl. | |||
| 2014-05-08 | Renaming new_induct -> induction; new_destruct -> destruct. | Hugo Herbelin | |
| 2014-05-08 | Little reorganization of generalize tactics code w/o semantic changes. | Hugo Herbelin | |
| Also removing trailing spaces. | |||
| 2014-05-08 | Cleanup code in pretyping/evarutil | Matthieu Sozeau | |
| 2014-05-08 | Fix performance problem with unification in presence of universes (bug ↵ | Matthieu Sozeau | |
| #3302) by considering Type i a ground term even when "i" is a flexible universe variable, using the infer_conv function to do the unification of universes. | |||
| 2014-05-08 | - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ↵ | Matthieu Sozeau | |
| evar_map in tactics, avoiding useless and potentially costly merge's of constraints. - Implement revert and generalize using the new tactics (not bound to syntax though, as they are not backwards-compatible yet). | |||
| 2014-05-08 | Avoid allocations in type_of_inductive | Matthieu Sozeau | |
| 2014-05-08 | Fast-path equality of sorts in compare_constr* | Matthieu Sozeau | |
| 2014-05-08 | Adapt the checker to polymorphic universes and projections (untested). | Matthieu Sozeau | |
| 2014-05-08 | Moving Dnet-related code to tactics/. | Pierre-Marie Pédrot | |
| 2014-05-08 | Fixing test-suite for bug #3043. | Pierre-Marie Pédrot | |
| 2014-05-08 | Fixing output test-suite: since universe polymorphism, the Print command | Pierre-Marie Pédrot | |
| shows the polymorphism status of the term. | |||
| 2014-05-08 | Code cleaning in Tacinterp: factorizing some uses of tclEVARS. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |