aboutsummaryrefslogtreecommitdiff
path: root/Makefile
AgeCommit message (Expand)Author
2002-11-04ajout d'une entrée au makefile pour faire toutes les theories sauf les realsletouzey
2002-10-15commit du calcul des dependances un peu plus robustebarras
2002-10-14*** empty log message ***desmettr
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...herbelin
2002-10-10Ajout ClassicalFactsherbelin
2002-10-07Lazy manuelles dans le codecoq
2002-10-07Make sure that bin/parser exists when checking that it worksbertot
2002-10-05Lazy experimentale temporaire...coq
2002-10-02*** empty log message ***desmettr
2002-10-01Adding the congruence closure tactics (CC and CCsolve).corbinea
2002-09-25*** empty log message ***desmettr
2002-09-18retablissement de Correctness (pas encore teste' cependant)filliatr
2002-08-19Pretty-printing preliminaire des modules, commandescoq
2002-08-02Modules dans COQ\!\!\!\!coq
2002-07-31*** empty log message ***desmettr
2002-07-31*** empty log message ***desmettr
2002-07-29*** empty log message ***desmettr
2002-07-18*** empty log message ***desmettr
2002-07-17ajout de make otags utilisant otags plutot que etagsletouzey
2002-07-17modification de make tags pourletouzey
2002-07-16MAJ Makefile pour Realsdesmettr
2002-07-15code retour de make checkcourant
2002-07-12*** empty log message ***desmettr
2002-07-05*** empty log message ***desmettr
2002-07-01*** empty log message ***desmettr
2002-07-01*** empty log message ***desmettr
2002-06-25*** empty log message ***desmettr
2002-06-20*** empty log message ***desmettr
2002-06-20ZArith_base, Zbool, Bool_natfilliatr
2002-06-19deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwffilliatr
2002-06-17*** empty log message ***desmettr
2002-06-11*** empty log message ***desmettr
2002-06-07extraction vers schemeletouzey
2002-06-07Adding file theories/ZArith/Zsqrt.v that contains a square root function.bertot
2002-06-05Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...herbelin
2002-06-04*** empty log message ***courant
2002-06-04'make check' echoue si au moins un test echoue.courant
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.vherbelin
2002-04-15integration de coq-inferior par Marco Maggesifilliatr
2002-04-05nouveau module Zdivfilliatr
2002-04-04resolution du pb d'efficacite du a Sign.add_named_declbarras
2002-03-27*** empty log message ***mohring
2002-03-22An intuitionistic first-order theorem prover -- JProver.huang
2002-03-13cleanconfig efface ocamldebug-v7filliatr
2002-03-12*** empty log message ***courant
2002-03-05ajout d'une entree 'binaries' pour recompiler coq mais pas les theoriesbarras
2002-03-04Big commit extraction:letouzey
2002-02-20Changé le nom du module Errors (errors.mli, errors.ml) en Cerrors parceddr
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras