aboutsummaryrefslogtreecommitdiff
path: root/Makefile
AgeCommit message (Expand)Author
2006-02-08Ajout bibliothèque String de Laurent Théryherbelin
2006-02-04code mortherbelin
2006-02-01New version of functional induction / inversion. By Julien Forest,coq
2006-01-31Ajout de fichiers d'interprétation de la syntaxe primitive pour string et charherbelin
2006-01-16dans la liste des cmo pour dev/printers.cma, manquait proofs/tacexpr.cmoletouzey
2006-01-04Restauration des commandes de débogage PrintConstr et PrintPureConstr (suite...herbelin
2005-12-30Correction dépendance g_prim.ml4/q_coqast.ml4herbelin
2005-12-26Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...herbelin
2005-12-26Achèvement suppression traducteur dans contrib/interfaceherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-12-25Utilisation de -notop pour imposer l'absence de module toplevelherbelin
2005-12-23Débranchement des parseurs de syntaxe v7herbelin
2005-12-20Abandon gestion des extensions de syntaxe de la v7 et du traducteur dans meta...herbelin
2005-12-15correction d'un bug dans le make installnarboux
2005-12-02Changement des named_contextgregoire
2005-11-18commited new ringbarras
2005-11-07Adds tools to help in defining new general recursive functionsbertot
2005-11-05option -w y finalement pas admise par ocamlc <= 3.08.2herbelin
2005-11-04Compatibilité ocaml 3.09herbelin
2005-08-17new congruencecorbinea
2005-07-15Subtac: traitement correct des existentielles et de la récursion.coq
2005-07-15reflexive tautocorbinea
2005-06-24dp: ajout des prédicats de sortescoq
2005-06-09dp: traitement des fixpointscoq
2005-05-25Forgot to remove a cmo.coq
2005-05-25Added subtac contrib.coq
2005-05-24dp: ajout du prouveur Zenoncoq
2005-05-20Interface vers outil de recherche Whelpherbelin
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2005-03-18appel de Simplify depuis Coqcoq
2005-03-16tactiques prouveurs premier ordre dans contrib/dp/coq
2005-03-11Ajout de COQLIB/user-contrib à l'installation pour insister sur la possibili...herbelin
2005-03-01clean de parser.optherbelin
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ...herbelin
2005-02-04Ajout g_xml.ml4 et cic2Xml.mlherbelin
2005-02-03Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursherbelin
2005-02-01Application du patch ebuild coq-8.0-r1 de la gentoo (uniformisation du Makefile)herbelin
2005-01-25Ajout dependance LIBCOQRUN pour coqide et coq-interfaceherbelin
2005-01-21Modification cible doc/coq.tex pour tenir des .mli qui n'existent pas toujour...herbelin
2005-01-03HUGE COMMITsacerdot
2005-01-02Pour permettre le chargement des printers en ocamldebug >= 3.07 : renommage s...herbelin
2004-12-27Remplacement du coeur d'omega (omega.ml) par la version plus générale utili...herbelin
2004-12-25Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...herbelin
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-11-15bug coqmktop avec libcoqrun.a en bytecodebarras
2004-11-05autorewrite moved from HIGHTACTICS to TACTICS (to implement Printingsacerdot
2004-10-20COMMITED BYTECODE COMPILERbarras
2004-10-18Tacred après Typingherbelin
2004-09-26no-assert en mode natifherbelin
2004-09-23error if binder was already definedbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 21:10:20 +0000