aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2000-12-14Bug sur commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1103 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Enfin trouvé la cause d'exception; suppression de la capsule de rattrapageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1102 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Ajout du répertoire config utilisé par System en localherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1053 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-04Ajout de constr_of_stringmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1044 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29ajout constr_displayfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1032 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29-I configmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1029 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Prise en compte qualidherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@963 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@954 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24Paramètrage de ocamldebug-v7 par configure à partir d'un 'template'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@949 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22Reparation bug mutuels indmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@916 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-11Gros hack pour afficher les universherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@846 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-02suppression des (* open Generic *)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-27g_natsyntax et g_zsyntax maintenant toujours linkesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@773 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-23MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@736 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-18MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@729 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-11MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@700 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-06MAJ pr_uniherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@666 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Commit malencontreux sur précédente versionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@655 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-04Mise en conformité nouveau Simpl pour Fixherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@654 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-03MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@641 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01Renommage AppL en Appherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@635 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-10-01MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@629 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@614 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-14MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@606 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-12MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@598 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-10Ajout d'un LetIn primitif.herbelin
Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-09-06Canonisation de certains noms dans Pretyping, Asterm et Safe_typingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@586 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-24MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@570 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@569 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-21bug discharge STRUCTURE; FrozenState supprimmes dans les ClosedSection -> ↵filliatr
.vo plus petits git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@514 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-02MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@491 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@484 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-18MAJ modifs Inductiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@448 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-05MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@428 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-04Nettoyage de l'interface de Pfeditherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@415 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03Ajout de PrintConstr pour debugdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@410 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-05-03renommage de certains printersherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@402 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-30MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@392 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@386 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-04-17Prise en compte du renommage des fonctions de Asttermherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@361 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-28Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en ↵herbelin
{pf_,}interp_constr* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@357 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-18bug discharge (work_alist contenanti plein de fois les memes choses)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@323 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-17Correction bug des réduction 'deltat' et renommage 'deltat' en 'evar'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@322 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-03-07Renommage ppterm0 --> pptermherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@293 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-26mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@286 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
- tactics/Equality - debug du discharge - constr_of_compattern implante vite fait / mal fait en attendant mieux - theories/Logic (ne passe pas entierrement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-07Restructuration printer et parserherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@270 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-01-07Restructuration diversesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@269 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
les fonctions sur les inductifs prennent maintenant des 'inductive' en paramètres; elle n'ont plus besoin de faire des appels dangereux aux find_m*type qui centralisent la levée de raise Induc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-14rattrapage exceptions autres que UserErrorfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@254 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:31:41 +0000