aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend.camlp4
Commit message (Collapse)AuthorAge
* majGravatar coq2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7768 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7586 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
* new congruenceGravatar corbinea2005-08-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7298 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
* 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
* 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
* tactiques prouveurs premier ordre dans contrib/dp/Gravatar coq2005-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout g_xml.ml4 et cic2Xml.mlGravatar herbelin2005-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6683 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6038 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5995 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5933 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-05-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5728 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5258 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-01-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5205 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground update + Linear removalGravatar corbinea2003-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4654 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression de newtautoGravatar corbinea2003-07-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4214 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ground major update ... mmm, sounds exciting !Gravatar corbinea2003-06-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4167 85f007b7-540e-0410-9357-904b9bb8a0f7
* moved engine.ml4 to ground.ml4, added option 'Ground Depth'Gravatar corbinea2003-05-26
| | | | | | | fixed utf8.vo dependency. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4078 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added the Ground tactic.Gravatar corbinea2003-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3955 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Ajout du traducteur nouvelle syntaxe *Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3760 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2003-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3720 85f007b7-540e-0410-9357-904b9bb8a0f7
* The contribution of Pierre Courtieu on generating specialized induction schemesGravatar bertot2003-02-27
| | | | | | | for recursive functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3710 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bringing Linear back to life (Still somewhat buggy).Gravatar corbinea2003-02-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).Gravatar corbinea2003-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
| | | | | | | | | | | | | | | - Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
| | | | | | | | | | | - Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding the congruence closure tactics (CC and CCsolve).Gravatar corbinea2002-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3061 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3022 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2002-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3021 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
* extraction vers schemeGravatar letouzey2002-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2771 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵Gravatar herbelin2002-05-29
| | | | | | commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
* contrib/interface/dad.ml4 had no real need of streams, it should have beenGravatar bertot2001-12-19
| | | | | | | | translated into a regular ml files like the others. This mistake is now corrected. The Makefile and dependency files are updated accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2345 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation du make depend et du .dependGravatar letouzey2001-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2334 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les réduction dans les hypothèses s'appliquent maintenant au corps de la ↵Gravatar herbelin2001-06-25
| | | | | | définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la ↵Gravatar herbelin2001-06-25
| | | | | | compilation native powerpc), le nouveau morceau étant g_ltac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de FieldGravatar delahaye2001-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1609 85f007b7-540e-0410-9357-904b9bb8a0f7
* réparation Correctness; options Extraction (changement de syntaxe)Gravatar filliatr2001-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1571 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout lemmes arithmetiquesGravatar mohring2001-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1557 85f007b7-540e-0410-9357-904b9bb8a0f7
* branchement extraction (bytecode seulement)Gravatar filliatr2001-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1509 85f007b7-540e-0410-9357-904b9bb8a0f7
* simplification du make depend; fonctions de stat. util. memoire dans ↵Gravatar filliatr2001-02-08
| | | | | | certains modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7
* calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)Gravatar filliatr2001-02-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1325 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jourGravatar filliatr2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1031 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2000-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@806 85f007b7-540e-0410-9357-904b9bb8a0f7
* compilation des fichiers ml4 sans GNUseriesGravatar filliatr2000-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@795 85f007b7-540e-0410-9357-904b9bb8a0f7
* - simplification Makefile (compilation des fichiers .ml'; pas encore parfaitGravatar filliatr2000-10-31
| | | | | | | | car on passe par les fichiers .ml) - Require Export enfin rétabli avec la bonne sémantique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@792 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 00:38:53 +0000