aboutsummaryrefslogtreecommitdiff
path: root/Makefile
AgeCommit message (Expand)Author
2006-03-13Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.msozeau
2006-03-08 r8623@thot: notin | 2006-03-08 12:40:57 +0100notin
2006-03-08 r8620@thot: notin | 2006-03-08 11:44:16 +0100notin
2006-03-05Modularisation des preuves concernant la logique classique, l'indiscernabilit...herbelin
2006-02-27dp: sortie Whyfilliatr
2006-02-22Add vernacular file for subtaccoq
2006-02-20Forgot a filecoq
2006-02-20Change in subtac modulescoq
2006-02-12Nettoyage Zmin.v, création Zmax.v et Zminmax.vherbelin
2006-02-08Julien:bertot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 23:03:19 +0000