| 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-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-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-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 | |
| 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 |