aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
Commit message (Expand)AuthorAge
* Adds a possibility to construct a term as if it had been parsed throughGravatar bertot2003-01-30
* Make sure the parser is compiled in native mode.Gravatar bertot2003-01-30
* Ajoute les directives pour créer aussi bin/coq-interface.optGravatar bertot2003-01-30
* pas de Xml.voGravatar filliatr2003-01-30
* on cree toujours le sous-repertoire tactics/Gravatar filliatr2003-01-24
* Ajout de LinearIntuition; Ajout de New(Tauto|Intuition|LinearIntuition).Gravatar corbinea2003-01-23
* removes all references to ctast.ml the Makefile has been updated accordingly.Gravatar bertot2003-01-22
* MAJ pour renommage RcompletGravatar desmettr2003-01-22
* Binome.v -> Binomial.vGravatar desmettr2003-01-21
* renommage de TAF.v en MVT.vGravatar desmettr2003-01-16
* Renommage de RealsB en RbaseGravatar desmettr2003-01-16
* bit vectorsGravatar filliatr2003-01-06
* setoids dans norealGravatar letouzey2002-12-09
* MAJGravatar herbelin2002-11-29
* Réorganisation de la librairie des réelsGravatar desmettr2002-11-27
* Réorganisation de la librairie des réelsGravatar desmettr2002-11-27
* Options make coqlight/ make install-coqlight pour les impatients...Gravatar desmettr2002-11-26
* Option pour compiler une version 'light' des réelsGravatar desmettr2002-11-26
* MAJGravatar herbelin2002-11-26
* Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...Gravatar herbelin2002-11-24
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* ajout d'une entrée au makefile pour faire toutes les theories sauf les realsGravatar letouzey2002-11-04
* commit du calcul des dependances un peu plus robusteGravatar barras2002-10-15
* *** empty log message ***Gravatar desmettr2002-10-14
* Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...Gravatar herbelin2002-10-13
* Ajout ClassicalFactsGravatar herbelin2002-10-10
* Lazy manuelles dans le codeGravatar coq2002-10-07
* Make sure that bin/parser exists when checking that it worksGravatar bertot2002-10-07
* Lazy experimentale temporaire...Gravatar coq2002-10-05
* *** empty log message ***Gravatar desmettr2002-10-02
* Adding the congruence closure tactics (CC and CCsolve).Gravatar corbinea2002-10-01
* *** empty log message ***Gravatar desmettr2002-09-25
* retablissement de Correctness (pas encore teste' cependant)Gravatar filliatr2002-09-18
* Pretty-printing preliminaire des modules, commandesGravatar coq2002-08-19
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* *** empty log message ***Gravatar desmettr2002-07-31
* *** empty log message ***Gravatar desmettr2002-07-31
* *** empty log message ***Gravatar desmettr2002-07-29
* *** empty log message ***Gravatar desmettr2002-07-18
* ajout de make otags utilisant otags plutot que etagsGravatar letouzey2002-07-17
* modification de make tags pourGravatar letouzey2002-07-17
* MAJ Makefile pour RealsGravatar desmettr2002-07-16
* code retour de make checkGravatar courant2002-07-15
* *** empty log message ***Gravatar desmettr2002-07-12
* *** empty log message ***Gravatar desmettr2002-07-05
* *** empty log message ***Gravatar desmettr2002-07-01
* *** empty log message ***Gravatar desmettr2002-07-01
* *** empty log message ***Gravatar desmettr2002-06-25
* *** empty log message ***Gravatar desmettr2002-06-20