aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
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
1999-12-14pretty-printers pour le debuggerfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@251 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-12Ajout pp pattern et rawtermherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@241 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-12modules et coqcfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@239 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-10indications pour les developpeursfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@231 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-10debug resetfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@229 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-05premier debugagefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@210 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-03renommage pour eviter pbm avec ocamldep (syntax error)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@199 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-03pour debugger dans le toplevel ocamlfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@197 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-02Modifs suite à intégration de class.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@192 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-01Intégration du Termast et du Retyping de HH, et modifications connexesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@185 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-26module Classops; ajout de fonctions dans Declare en consequencefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@152 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-26style utilise dans le codefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@146 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-24Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@132 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-23modules Indrec, Tacentries, Hiddentacfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@131 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-22module Wcclausenvfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@130 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-19modules Bij, Gmapl, Stockfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@125 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-11-19discriminations netsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@123 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-20modules Evar_refiner et Typing_evfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@110 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-14module Proof_treesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@104 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-10-13mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@101 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-27ajout des constraintes pendant le chargement d'un module (load)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@81 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-25ensembles de contraintes d'universfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@78 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:38:03 +0000