aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
Commit message (Expand)AuthorAge
...
* Made pretyping a functor over a coercion implementation. Pretyping.Default us...Gravatar msozeau2006-03-22
* - Réintroduction d'un parseur de pattern (q_constr.ml4) à usage deGravatar herbelin2006-03-22
* Bug BYTEFLAGS pour compilation bin/parserGravatar herbelin2006-03-18
* ajout d'un debut de proprietes pour les FSetWeakGravatar letouzey2006-03-17
* Ajout de theories/FSets contenant la partie "light" de FSets et FMap:Gravatar letouzey2006-03-15
* r8637@thot: notin | 2006-03-14 16:00:49 +0100Gravatar notin2006-03-14
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
* r8623@thot: notin | 2006-03-08 12:40:57 +0100Gravatar notin2006-03-08
* r8620@thot: notin | 2006-03-08 11:44:16 +0100Gravatar notin2006-03-08
* 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