aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
Commit message (Expand)AuthorAge
* Modularisation des preuves concernant la logique classique, l'indiscernabilit...Gravatar herbelin2006-03-05
* dp: sortie WhyGravatar filliatr2006-02-27
* Add vernacular file for subtacGravatar coq2006-02-22
* Forgot a fileGravatar coq2006-02-20
* Change in subtac modulesGravatar coq2006-02-20
* Nettoyage Zmin.v, création Zmax.v et Zminmax.vGravatar herbelin2006-02-12
* Julien:Gravatar bertot2006-02-08
* Ajout bibliothèque String de Laurent ThéryGravatar herbelin2006-02-08
* code mortGravatar herbelin2006-02-04
* New version of functional induction / inversion. By Julien Forest,Gravatar coq2006-02-01
* Ajout de fichiers d'interprétation de la syntaxe primitive pour string et charGravatar herbelin2006-01-31
* dans la liste des cmo pour dev/printers.cma, manquait proofs/tacexpr.cmoGravatar letouzey2006-01-16
* Restauration des commandes de débogage PrintConstr et PrintPureConstr (suite...Gravatar herbelin2006-01-04
* Correction dépendance g_prim.ml4/q_coqast.ml4Gravatar herbelin2005-12-30
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Achèvement suppression traducteur dans contrib/interfaceGravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Utilisation de -notop pour imposer l'absence de module toplevelGravatar herbelin2005-12-25
* Débranchement des parseurs de syntaxe v7Gravatar herbelin2005-12-23
* Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...Gravatar herbelin2005-12-20
* correction d'un bug dans le make installGravatar narboux2005-12-15
* Changement des named_contextGravatar gregoire2005-12-02
* commited new ringGravatar barras2005-11-18
* Adds tools to help in defining new general recursive functionsGravatar bertot2005-11-07
* option -w y finalement pas admise par ocamlc <= 3.08.2Gravatar herbelin2005-11-05
* Compatibilité ocaml 3.09Gravatar herbelin2005-11-04
* new congruenceGravatar corbinea2005-08-17
* Subtac: traitement correct des existentielles et de la récursion.Gravatar coq2005-07-15
* reflexive tautoGravatar corbinea2005-07-15
* dp: ajout des prédicats de sortesGravatar coq2005-06-24
* dp: traitement des fixpointsGravatar coq2005-06-09
* Forgot to remove a cmo.Gravatar coq2005-05-25
* Added subtac contrib.Gravatar coq2005-05-25
* dp: ajout du prouveur ZenonGravatar coq2005-05-24
* Interface vers outil de recherche WhelpGravatar herbelin2005-05-20
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* appel de Simplify depuis CoqGravatar coq2005-03-18
* tactiques prouveurs premier ordre dans contrib/dp/Gravatar coq2005-03-16
* Ajout de COQLIB/user-contrib à l'installation pour insister sur la possibili...Gravatar herbelin2005-03-11
* clean de parser.optGravatar herbelin2005-03-01
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* Ajout g_xml.ml4 et cic2Xml.mlGravatar herbelin2005-02-04
* Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursGravatar herbelin2005-02-03
* Application du patch ebuild coq-8.0-r1 de la gentoo (uniformisation du Makefile)Gravatar herbelin2005-02-01
* Ajout dependance LIBCOQRUN pour coqide et coq-interfaceGravatar herbelin2005-01-25
* Modification cible doc/coq.tex pour tenir des .mli qui n'existent pas toujour...Gravatar herbelin2005-01-21
* HUGE COMMITGravatar sacerdot2005-01-03
* Pour permettre le chargement des printers en ocamldebug >= 3.07 : renommage s...Gravatar herbelin2005-01-02
* Remplacement du coeur d'omega (omega.ml) par la version plus générale utili...Gravatar herbelin2004-12-27
* Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...Gravatar herbelin2004-12-25