| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-05-20 | Moving (e)transitivity out of the AST. | Pierre-Marie Pédrot | |
| 2014-05-20 | Tactics declared through TACTIC EXTEND that are of the form | Pierre-Marie Pédrot | |
| "foobar" constr(x1) ... constr(xn) are now defined as pure Ltac definitions, and do not add grammar nor printing rules. This partially relies on a hack consisting in retrieving the arguments in the tactic environment rather than as directly passed to the TacExtend node. | |||
| 2014-05-20 | Tentative to add constr-using primitive tactics without grammar rules. | Pierre-Marie Pédrot | |
| We eta-expand primitive Ltac functions, and instead of feeding TacExtend directly with its arguments, we use the environment to retrieve them. Some tactics from the AST were also moved away and made using this mechanism. | |||
| 2014-05-18 | Revert "Fix Qcanon after changes on injection." | Maxime Dénès | |
| This reverts commit f3b3b6e4d01080da4f0ce37a06553769e9588d0e. | |||
| 2014-05-18 | When discrimination is not possible, try to project. | Maxime Dénès | |
| Example: Inductive Pnat : Prop := O | S : Pnat -> Pnat. Variable m n : Pnat. Goal S (S O) = S O -> False. intros H; injection H. now deduces S O = O instead of failing with an error message. | |||
| 2014-05-18 | Suggest Set Injection On Proofs in error message for injection. | Maxime Dénès | |
| 2014-05-18 | Restored old behavior of injection on proofs by default. | Maxime Dénès | |
| Use Set Injection On Proof to enable the new behavior. | |||
| 2014-05-17 | Adding way to get the list of the accepted tactic notation arguments. | Pierre-Marie Pédrot | |
| 2014-05-17 | Fixing coqdep_boot warning relative to unknown ML files that were in tactics. | Pierre-Marie Pédrot | |
| 2014-05-17 | Fixing Camlp4 compilation | Pierre-Marie Pédrot | |
| 2014-05-16 | Revert "Decent error message when a constant is not found" | Enrico Tassi | |
| This reverts commit c4bdf93e358b97b32e0d80d6c7d1b79a2ece1dc2. | |||
| 2014-05-16 | More fixes of unification with primitive projections (missed cases during ↵ | Matthieu Sozeau | |
| the merge). Obligations are not necessarily opaque. | |||
| 2014-05-16 | Declare: fix Future management | Enrico Tassi | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |