aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend
Commit message (Expand)AuthorAge
* remplace Zarith par ZArithGravatar mohring2001-04-19
* *** empty log message ***Gravatar courant2001-04-19
* Ajout de FieldGravatar delahaye2001-04-19
* Adding files for the production of textual explanations as used in pcoq.Gravatar bertot2001-04-18
* Modified searchPattern. Before this correction, constructors were overlooked,Gravatar bertot2001-04-10
* réparation Correctness; options Extraction (changement de syntaxe)Gravatar filliatr2001-04-10
* Ajout lemmes arithmetiquesGravatar mohring2001-04-08
* mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4Gravatar filliatr2001-04-05
* renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...Gravatar filliatr2001-04-04
* Adding the dependencies for the parser that is used in the interface pcoq.Gravatar bertot2001-04-04
* dependencies required for contrib/interfaceGravatar bertot2001-04-04
* branchement extraction (bytecode seulement)Gravatar filliatr2001-03-30
* amelioration de la structure des universGravatar barras2001-03-28
* mise a jourGravatar filliatr2001-03-27
* mise a jourGravatar filliatr2001-03-23
* extraction naive de fix et caseGravatar filliatr2001-03-20
* Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationGravatar herbelin2001-03-11
* module Explore générique et réécriture EAuto avec ce module; occur check ...Gravatar filliatr2001-03-05
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* nouvelle implantation de la reductionGravatar barras2001-03-01
* mise a jourGravatar filliatr2001-02-26
* Stdlib -> Coqlib, Stock disparaitGravatar herbelin2001-02-14
* simplification du make depend; fonctions de stat. util. memoire dans certains...Gravatar filliatr2001-02-08
* Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dirGravatar herbelin2001-02-07
* mise en place extractionGravatar filliatr2001-02-06
* mise a jourGravatar filliatr2001-02-06
* MAJGravatar herbelin2001-02-06
* calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)Gravatar filliatr2001-02-05
* MAJGravatar herbelin2001-01-30
* Les Objdef introduisent une convertibilité avec les projections dans le test...Gravatar herbelin2001-01-30
* Ré-introduction des implicites à la volée dans la définition des inductifsGravatar herbelin2001-01-27
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* Nouveau module pour centraliser les chemins des constantes globales utilisée...Gravatar herbelin2001-01-19
* Pattern sera mieux dans Pretyping; relâchement head_pattern_boundGravatar herbelin2000-12-26
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Debut de reparation de simplGravatar mohring2000-12-11
* MAJGravatar herbelin2000-12-05
* Portage d'AutoRewriteGravatar delahaye2000-12-02
* mise a jourGravatar filliatr2000-11-29
* MAJGravatar herbelin2000-11-29
* MAJGravatar herbelin2000-11-26
* MAJGravatar filliatr2000-11-24
* SearchPattern et SearchRewriteGravatar filliatr2000-11-24
* Ajout d'une syntaxe pour Reals.Gravatar mayero2000-11-23
* MAJGravatar herbelin2000-11-23
* retablissement de line_oriented_parser pour YvesGravatar filliatr2000-11-22
* des proofs/macros qui trainaient dans le Makefile et le .dependGravatar filliatr2000-11-22
* separation calcul des implicites et declaration des constantes / inductifs / ...Gravatar filliatr2000-11-21
* MAJGravatar herbelin2000-11-20
* mise a jourGravatar filliatr2000-11-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 08:40:13 +0000