aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* - Débogueur: positionnement de set_detype_anonymous pour ne pasGravatar herbelin2007-08-29
| | | | | | | | | échouer sur les Rel liées a des Anonymous et export de l'instance des evars vers le printeur du débogueur. - Suppression d'un reste de code mort lié à la V7 dans pretyping.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10102 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction bug dans syntaxe des match (liste de motifs vide était acceptée)Gravatar herbelin2007-08-22
| | | | | | | - Des open en plus dans le débogueur-traceur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10083 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add glob.dump to Makefile the recommended way and document theGravatar lmamane2007-07-25
| | | | | | | recommended way more explicitly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10050 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorganise cleaning targetsGravatar lmamane2007-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10012 85f007b7-540e-0410-9357-904b9bb8a0f7
* A cleaner solution to "make deletes .ml4.d files -> infinite loop" problemGravatar lmamane2007-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10010 85f007b7-540e-0410-9357-904b9bb8a0f7
* New bootstrapping, improved, Makefile systemGravatar corbinea2007-07-13
| | | | | | | Documented in dev/doc/build-system.txt . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9992 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2007-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9844 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques exemples sur l'asymétrie de la conversionGravatar herbelin2007-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9814 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
| | | | | | | | | Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in", "erewrite" et "erewrite in". Correction au passage des bugs #1461 et #1522). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771Gravatar herbelin2007-04-18
| | | | | | | | | | | (les let-in étaient comptés comme des produits, introduisant une incohérence sur le nombre de produits à instancier dans les lemmes appelés par apply). - Export simplest_eapply pour utilisation dans Sophia/RecursiveDefinition. - Doc développeur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9785 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rajout du mot Fix dans le printerGravatar vsiles2007-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9779 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retablissement de Fix dans print_pure_constr Gravatar vsiles2007-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9778 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allègement de l'affichage des références par le printer si possibleGravatar herbelin2007-01-22
| | | | | | | | | | | | (on garde des noms de la forme IND(name,i) et CONSTR(name,i,j) que lorsqu'on ne sait pas le bon nom, i.e. pour les IND mutuels autres que le premier et pour tous les constructeurs). Pour un affichage complètement explicite des noms avec ocamldebug, charger maintenant set_raw_db en plus de db. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9515 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export de l'afficheur de substitutions de noms de modules pour le débogueurGravatar herbelin2007-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9504 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2006-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9390 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2006-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9322 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplification ocamldebug (coq-debug-programs.out obsolète)Gravatar herbelin2006-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9241 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reactivation des outils de developpement de JacekGravatar herbelin2006-09-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9190 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tout petit bug d'affichage dans constr_display (top_printers)Gravatar herbelin2006-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9161 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
| | | | | | | | | | | | | | | | | | | Part contre ces cas sont detruis dans les "Definition" (pas dans les "Lemma") je comprends pas ou ils sont enlev'e... Si une id'ee ... - Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland. - Meilleur compilation des coinductifs, on utilise maintenant vraimment du lazy. - Enfin un peu plus de doc dans le code de la vm. Benjamin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ fichier dev/doc/changes.txtGravatar herbelin2006-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8946 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix broken paths.Gravatar msozeau2006-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8874 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added contrib/funind to the path for ocamldebug-coqGravatar courtieu2006-05-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8864 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise à jour dev/doc/changes.txt et ajout d'un mot sur TACTIC EXTENDGravatar herbelin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8857 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration dossier dev et mise à jour de certaines documentationsGravatar herbelin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8856 85f007b7-540e-0410-9357-904b9bb8a0f7
* PÃréouverture de la plupart des fichis pour éviter d'avoir à qualifierGravatar herbelin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8846 85f007b7-540e-0410-9357-904b9bb8a0f7
* Comments about profilingGravatar herbelin2006-05-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Standardisation du nom des méthodes de EvdGravatar herbelin2006-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵Gravatar notin2006-04-28
| | | | | | 'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Official MoWGLI definition of CIC dtdGravatar herbelin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8753 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'entrée devdoc dans le Makefile principal et modification ↵Gravatar notin2006-04-27
| | | | | | en conséquence du Makefile dans dev/doc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8750 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ debugging (et arrêt support version française)Gravatar herbelin2006-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8643 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement du répertoire doc dans devGravatar notin2006-03-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8140 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout ppenvGravatar herbelin2006-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7952 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plutôt pas de contraction des match dans le déboggueurGravatar herbelin2006-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7951 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout printer Idset.tGravatar herbelin2006-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7947 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
| | | | | | | et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restauration des commandes de débogage PrintConstr et PrintPureConstr ↵Gravatar herbelin2006-01-04
| | | | | | (suite): correction des dépendances (et notamment non-dépendance en unix.cma) pour la création de printers.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7787 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage concis des locations (si jamais ppterm/pprawterm sont débranchés)Gravatar herbelin2006-01-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7786 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remise en place des commandes vernaculaires PrintConstr et PrintPureConstr ↵Gravatar herbelin2006-01-04
| | | | | | (débranchées depuis mars 01) + affichage plus concis des locations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7785 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2005-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7750 85f007b7-540e-0410-9357-904b9bb8a0f7
* Analyse des tests automatiques de compilation des contributionsGravatar herbelin2005-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7749 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@7734 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ restructuration constrintern.mlGravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7711 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
* 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
* Ajout constant printerGravatar herbelin2005-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6735 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added bigint printerGravatar herbelin2005-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6733 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 08:22:32 +0000