| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-03-21 | Creating a dedicated ltac/ folder for Hightactics. | Pierre-Marie Pédrot | |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-01-20 | Update copyright headers. | Maxime Dénès | |
| 2016-01-02 | Separation of concern in TacAlias API. | Pierre-Marie Pédrot | |
| The TacAlias node now only contains the arguments fed to the tactic notation. The binding variables are worn by the tactic representation in Tacenv. | |||
| 2015-12-21 | Using dynamic values in tactic evaluation. | Pierre-Marie Pédrot | |
| 2015-06-01 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-05-15 | Granting wish #4048: Locate Ltac prints the source of redefined Ltac. | Pierre-Marie Pédrot | |
| 2015-05-15 | Merge v8.5 into trunk | Hugo Herbelin | |
| Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API) | |||
| 2015-05-11 | Adding a test to check whether two tactic notations conflict. | Pierre-Marie Pédrot | |
| 2015-05-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-04-23 | Remove almost all the uses of string concatenation when building error messages. | Guillaume Melquiond | |
| Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure. | |||
| 2015-02-10 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-02 | Removing dead code. | Pierre-Marie Pédrot | |
| 2015-01-23 | Splitting ML tactics in one function per grammar entry. | Pierre-Marie Pédrot | |
| Furthermore, ML tactic dispatch is not done according to the type of its argument anymore. | |||
| 2015-01-21 | Embedding the index of the ML tactic entry in the Tacexpr AST. | Pierre-Marie Pédrot | |
| This will allow to get rid of the fragile mechanism of discriminating which entry to call depending on the dynamic type of its arguments. | |||
| 2015-01-12 | Update headers. | Maxime Dénès | |
| 2014-12-16 | Fixing CAMLP4 compilation. | Pierre-Marie Pédrot | |
| 2014-10-01 | Fixing nice printing of error reporting with ml tactics bound to ltac names. | Hugo Herbelin | |
| 2014-09-03 | Fixing bug #2818. | Pierre-Marie Pédrot | |
| Local Ltac definitions do not register their name in the nametab anymore, thus elegantly solving the bug. The tactic body remains accessible from the tactic engine, but the name is rendered meaningless to the userside. | |||
| 2014-09-03 | Useless hooks in Tacintern. | Pierre-Marie Pédrot | |
| 2014-09-03 | Code simplification in Tacenv. | Pierre-Marie Pédrot | |
| 2014-08-31 | Getting rid of atomic tactics in Tacenv. | Pierre-Marie Pédrot | |
| ML tactics that may be used as simple identifiers are now declared as a true Ltac entry pertaining to the module that contains the Declare ML Module statement. | |||
| 2014-08-31 | Moving code of tactic interpretation from Tacenv to Vernacentries. | Pierre-Marie Pédrot | |
| This allows to directly register globtactics in the Tacenv API, without having to resort to any internalization function. | |||
| 2014-08-18 | Moving the TacExtend node from atomic to plain tactics. | Pierre-Marie Pédrot | |
| Also taking advantage of the change to rename it into TacML. Ultimately should allow ML tactic to return values. | |||
| 2014-08-07 | Removing the "constructor" tactic from the AST. | Pierre-Marie Pédrot | |
| 2014-07-27 | Code cleaning in Tacenv. | Pierre-Marie Pédrot | |
| 2014-07-27 | Qualified ML tactic names. The plugin name is used to discriminate | Pierre-Marie Pédrot | |
| potentially conflicting tactics names from different plugins. | |||
| 2014-06-30 | Useless keeping of dirpath in tactic aliases. | Pierre-Marie Pédrot | |
| 2014-06-06 | Moving the [split] tactic out of the AST. | Pierre-Marie Pédrot | |
| 2014-06-02 | Removing symmetry from the atomic tactics. | Pierre-Marie Pédrot | |
| 2014-05-21 | Allowing Ltac definitions that may be unusable because of a built-in | Pierre-Marie Pédrot | |
| parsing rule. | |||
| 2014-05-21 | Moving left & right tactics out of the AST. | Pierre-Marie Pédrot | |
| 2014-05-16 | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot | |
| "coretactics.ml4" file. | |||
| 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-01-10 | Fix bug#2080: error message on Ltac name clash with primitive tactics | xclerc | |
| 2013-11-10 | Centralizing the Ltac-defining functions in Tacenv. | ppedrot | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17080 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2013-11-10 | Removing the dependency of every level of tactic ATSs on glob_tactic_expr. | ppedrot | |
| Instead of putting the body directly in the AST, we register it in a table. This time it should work properly. Tactic notation are given kernel names to ensure the unicity of their contents. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17079 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2013-11-09 | Revert the previous commit. It broke Coq compilation. | ppedrot | |
| Tactics notation interpretation was messed up because of the use of identical keys for different notations. All my tentative fixes were unsuccessful, so better blankly revert the commit for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17078 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2013-11-09 | Removing the dependency of every level of tactic ATSs on glob_tactic_expr. | ppedrot | |
| Instead of putting the body directly in the AST, we register it in a table. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17077 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |