aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend
Commit message (Collapse)AuthorAge
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵Gravatar herbelin2005-12-26
| | | | | | G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur ↵Gravatar herbelin2005-12-26
| | | | | | (mcanismes de renommage des noms de constantes, de module, de ltac et de certaines variables lies de lemmes et de tactiques, mcanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7736 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7730 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7690 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7678 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7663 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement des named_contextGravatar gregoire2005-12-02
| | | | | | | | Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7621 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7586 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7576 85f007b7-540e-0410-9357-904b9bb8a0f7
* A la demande de Julien ForestGravatar letouzey2005-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7573 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7541 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7529 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications in the .depend files for the contrib/recdef directoryGravatar bertot2005-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7528 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds tools to help in defining new general recursive functionsGravatar bertot2005-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7527 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7494 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7474 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7367 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-08-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7299 85f007b7-540e-0410-9357-904b9bb8a0f7
* new congruenceGravatar corbinea2005-08-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7298 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7267 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7264 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7262 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7238 85f007b7-540e-0410-9357-904b9bb8a0f7
* Subtac: traitement correct des existentielles et de la récursion.Gravatar coq2005-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7237 85f007b7-540e-0410-9357-904b9bb8a0f7
* reflexive tautoGravatar corbinea2005-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7233 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-07-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7227 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-07-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7224 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-07-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7220 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7167 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-06-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7145 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-06-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7131 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7122 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-06-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7114 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7075 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added subtac contrib.Gravatar coq2005-05-25
| | | | | | | Added some debug printer in termops. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7073 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7070 85f007b7-540e-0410-9357-904b9bb8a0f7
* dp: ajout du prouveur ZenonGravatar coq2005-05-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7066 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7054 85f007b7-540e-0410-9357-904b9bb8a0f7
* New command: "Print Ltac qualid" to print user defined tactics.Gravatar sacerdot2005-05-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7053 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7043 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7035 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7031 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵Gravatar herbelin2005-05-17
| | | | | | aux niveaux syntaxiques des tacticielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7023 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6951 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6920 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6885 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-03-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6876 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de l'axiome du but prouve par la tactique simplifiGravatar coq2005-03-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6875 85f007b7-540e-0410-9357-904b9bb8a0f7