aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2006-09-29Reactivation des outils de developpement de Jacekherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9190 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-22Tout petit bug d'affichage dans constr_display (top_printers)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9161 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-22- Ajout d'un cast vm dans la syntaxe : x <: t bgregoir
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
2006-06-10MAJ fichier dev/doc/changes.txtherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8946 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-29Fix broken paths.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8874 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-26Added contrib/funind to the path for ocamldebug-coqcourtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8864 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23Mise à jour dev/doc/changes.txt et ajout d'un mot sur TACTIC EXTENDherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8857 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23Restructuration dossier dev et mise à jour de certaines documentationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8856 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23PÃréouverture de la plupart des fichis pour éviter d'avoir à qualifierherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8846 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-11Comments about profilingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8806 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Standardisation du nom des méthodes de Evdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵notin
'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Official MoWGLI definition of CIC dtdherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8753 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Suppression de l'entrée devdoc dans le Makefile principal et modification ↵notin
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
2006-03-17MAJ debugging (et arrêt support version française)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8643 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-06Deplacement du répertoire doc dans devnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8140 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30Ajout ppenvherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7952 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-30Plutôt pas de contraction des match dans le déboggueurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7951 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-29Ajout printer Idset.therbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7947 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
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
2006-01-04Restauration des commandes de débogage PrintConstr et PrintPureConstr ↵herbelin
(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
2006-01-04Affichage concis des locations (si jamais ppterm/pprawterm sont débranchés)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7786 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-04Remise en place des commandes vernaculaires PrintConstr et PrintPureConstr ↵herbelin
(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
2005-12-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7750 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-28Analyse des tests automatiques de compilation des contributionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7749 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵herbelin
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
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur ↵herbelin
(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
2005-12-23MAJ restructuration constrintern.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7711 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-02Changement des named_contextgregoire
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
2005-05-25Added subtac contrib.coq
Added some debug printer in termops. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7073 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Ajout constant printerherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6735 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Added bigint printerherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6733 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02Réactivation d'un outil d'affichage pour le débogueur compatible avec ↵herbelin
ocaml 3.07 et 3.08 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6549 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02Découpage des printers pour ne pas avoir de dépendances en la vm dans les ↵herbelin
printers de ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6545 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-31Remplacement ocamldebug-v7 par lien symbolique ne marche pas, finalement, ↵herbelin
création du lien par configure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6535 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-31Remplacement ocamldebug-v7 par ocamldebug-coq (2ème)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6534 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-29Ajout printer bigintherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6523 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-23MAJ coq v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6496 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-23MAJ coq v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6495 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-23Renommage de ocamldebug-v7 en ocamldebug-coq (pour passage à la v8)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6494 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-23Renommage de ocamldebug-v7 en ocamldebug-coq (pour passage à la v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6493 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-12Changement dans les boxed values .gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-17restructuration des printers: proofs passe avant parsingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-15hiding the meta_map in evar_defsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08unification encore...barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6085 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-03Header V8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6016 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 08:58:30 +0000