aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/subtac
Commit message (Expand)AuthorAge
* New files for subtacGravatar coq2006-03-05
* Work on recursive definitionsGravatar coq2006-02-22
* Add vernacular file for subtacGravatar coq2006-02-22
* Work with binder lists, problem of tyconsGravatar coq2006-02-21
* Latest fixes, should work fine now for non recursive definitions, although st...Gravatar coq2006-02-21
* Fix minor bugGravatar coq2006-02-20
* Forgot a fileGravatar coq2006-02-20
* Monday work, working with coercions and implicit argsGravatar coq2006-02-20
* Forgot another file...Gravatar coq2006-02-20
* Forgot one fileGravatar coq2006-02-20
* Rewrite of the subtac tactic, needs some work on implicit arguments.Gravatar coq2006-02-20
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...Gravatar herbelin2005-12-26
* Changement des named_contextGravatar gregoire2005-12-02
* Subtac: traitement correct des existentielles et de la récursion.Gravatar coq2005-07-15
* General recursive definitions on well founded orders supportGravatar coq2005-07-13
* Add a guard for V7 mode, CVS compiles cleanly again :)Gravatar coq2005-05-26
* Added subtac contrib.Gravatar coq2005-05-25
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-01 10:55:01 +0000