aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Moving (e)transitivity out of the AST.Gravatar Pierre-Marie Pédrot2014-05-20
|
* Tactics declared through TACTIC EXTEND that are of the formGravatar Pierre-Marie Pédrot2014-05-20
| | | | | | | | | "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.
* Tentative to add constr-using primitive tactics without grammar rules.Gravatar Pierre-Marie Pédrot2014-05-20
| | | | | | | | 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.
* Revert "Fix Qcanon after changes on injection."Gravatar Maxime Dénès2014-05-18
| | | | This reverts commit f3b3b6e4d01080da4f0ce37a06553769e9588d0e.
* When discrimination is not possible, try to project.Gravatar Maxime Dénès2014-05-18
| | | | | | | | | | | | 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.
* Suggest Set Injection On Proofs in error message for injection.Gravatar Maxime Dénès2014-05-18
|
* Restored old behavior of injection on proofs by default.Gravatar Maxime Dénès2014-05-18
| | | | Use Set Injection On Proof to enable the new behavior.
* Adding way to get the list of the accepted tactic notation arguments.Gravatar Pierre-Marie Pédrot2014-05-17
|
* Fixing coqdep_boot warning relative to unknown ML files that were in tactics.Gravatar Pierre-Marie Pédrot2014-05-17
|
* Fixing Camlp4 compilationGravatar Pierre-Marie Pédrot2014-05-17
|
* Revert "Decent error message when a constant is not found"Gravatar Enrico Tassi2014-05-16
| | | | This reverts commit c4bdf93e358b97b32e0d80d6c7d1b79a2ece1dc2.
* More fixes of unification with primitive projections (missed cases during ↵Gravatar Matthieu Sozeau2014-05-16
| | | | | | the merge). Obligations are not necessarily opaque.
* Declare: fix Future managementGravatar Enrico Tassi2014-05-16
|
* Decent error message when a constant is not foundGravatar Enrico Tassi2014-05-16
|
* Fix unification of non-unfoldable primitive projections in evarconv.Gravatar Matthieu Sozeau2014-05-16
|
* Moving argument-free tactics out of the AST into a dedicatedGravatar Pierre-Marie Pédrot2014-05-16
| | | | "coretactics.ml4" file.
* Slightly better printer for native ML tactics, in order to disambiguateGravatar Pierre-Marie Pédrot2014-05-16
| | | | them.
* Tactics defined through TACTIC EXTEND that are only defined as a string doGravatar Pierre-Marie Pédrot2014-05-16
| | | | | not create grammar and printing rules anymore, they define Ltac entries in the module that declares them instead.
* Another try at close_proof that should behave better w.r.t. exception handling.Gravatar Matthieu Sozeau2014-05-16
|
* heads: avoid forcing opaque proofsGravatar Enrico Tassi2014-05-15
|
* poly: remove unused attribute to STM nodes and vernac classificaitonGravatar Enrico Tassi2014-05-15
|
* Polymorphic Lemmas are like Defined ones for STMGravatar Enrico Tassi2014-05-15
|
* Future: better error messageGravatar Enrico Tassi2014-05-15
|
* Fix the behaviour of ML tactic notations w.r.t. Imports by making themGravatar Pierre-Marie Pédrot2014-05-13
| | | | substitutive.
* Test-suite for bug #3259.Gravatar Pierre-Marie Pédrot2014-05-13
|
* Rewritten the sorting algorithm for universes with a better complexity.Gravatar Pierre-Marie Pédrot2014-05-13
| | | | | | | | 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.
* Update various polyproj bugs w.r.t. latest trunkGravatar Jason Gross2014-05-12
|
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
| | | | | | | | | | | | | 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.
* Moving the ML tactic extension mechanism to a Libobject-based one.Gravatar Pierre-Marie Pédrot2014-05-12
|
* Plugin names must be declared in the header of .ml4 file, be they static orGravatar Pierre-Marie Pédrot2014-05-12
| | | | dynamic. This is done with the "DECLARE PLUGIN \"name\"" macro.
* Adding the possibility for ML modules to declare functions to be called atGravatar Pierre-Marie Pédrot2014-05-12
| | | | | caching time, i.e. when the Declare ML Module command is evaluated. This can be used by both static and dynamic plugins.
* Fixing the undocumented -dumpgraphbox option of coqdep.Gravatar Pierre-Marie Pédrot2014-05-12
|
* Using Maps to handle imports in Safe_typing. The order is irrelevant indeed,Gravatar Pierre-Marie Pédrot2014-05-11
| | | | and the lookup operation proved to be costly when dealing with big libraries.
* Eliminating a potentially quadratic behaviour in Require, by using mapsGravatar Pierre-Marie Pédrot2014-05-11
| | | | instead of lists to test if a library has already been encountered.
* Add appropriate Fail(s) to opened bugsGravatar Jason Gross2014-05-10
| | | | | | | | 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.
* Move opened bugs to bugs/openedGravatar Jason Gross2014-05-10
|
* Add more regression tests for univ poly/prim projGravatar Jason Gross2014-05-10
| | | | | | | | | | | 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.
* Code cleaning & factorizing functions in Equality.Gravatar Pierre-Marie Pédrot2014-05-09
|
* Update and start testing rewrite-in-type code.Gravatar Matthieu Sozeau2014-05-09
|
* More documentation of new features in CHANGE.Gravatar Pierre-Marie Pédrot2014-05-09
|
* Refresh universes for Ltac's type_of, as the term can be used anywhere,Gravatar Matthieu Sozeau2014-05-09
| | | | fixing two opened bugs from HoTT/coq.
* Merge branch 'working-polyproj-tests' of https://github.com/JasonGross/coq ↵Gravatar Matthieu Sozeau2014-05-09
|\ | | | | | | into JasonGross-working-polyproj-tests
* | Fix second-order matching to properly check that the predicate found byGravatar Matthieu Sozeau2014-05-09
| | | | | | | | | | abstraction has the right type. Fixes bug# 3306. Add test-suite files for bugs 3305 and 3306.
* | Restore implicit arguments of irreflexivity (fixes bug #3305).Gravatar Matthieu Sozeau2014-05-09
| |
* | Reuse universe level substitutions for template polymorphism, fixing performanceGravatar Matthieu Sozeau2014-05-09
| | | | | | | | problem with hashconsing at the same time. This fixes bug# 3302.
* | Encapsulating some clausenv uses. This simplifies the control flow of someGravatar Pierre-Marie Pédrot2014-05-08
| | | | | | | | tactics.
* | Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."Gravatar Hugo Herbelin2014-05-08
| | | | | | | | | | | | | | (made push command with wrong local ref; leaving control to Matthieu on new revert) This reverts commit b797ba85b7b0f82d66af5629ccf6f75d90dda99a.
* | Avoid "revert" to retype-check the goal, and move it to a "new" tactic.Gravatar Hugo Herbelin2014-05-08
| |
* | Typo reference manualGravatar Hugo Herbelin2014-05-08
| |
* | Isolating a function "make_abstraction", new name of "letin_abstract",Gravatar Hugo Herbelin2014-05-08
| | | | | | | | which compute an abstraction of the goal over a term or a pattern.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 10:43:29 +0000