aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals
AgeCommit message (Expand)Author
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
2002-04-02Optimisationdesmettr
2002-04-02Suppression PI_lb et PI_ubdesmettr
2002-04-02Suppression Fielddesmettr
2002-03-29sans utiliser Fielddesmettr
2002-03-29Suppression des invocations a Fielddesmettr
2002-03-22Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de Z...herbelin
2002-03-21Intuition ne fait plus de Unfold des constantes (il faut les fairecourant
2002-03-20Intuition now takes an (optional) tactic as parameter. This tactic iscourant
2002-03-19Exportation de SplitRmult et SplitAbsoludelahaye
2002-03-17Field ne fait maintenant que les reductions necessairesdelahaye
2002-03-07*** empty log message ***desmettr
2002-02-14option -dump-glob pour coqdocfilliatr
2002-01-07Ajout en-têteherbelin
2001-12-21Passage coqwebherbelin
2001-12-19*** empty log message ***desmettr
2001-12-07*** empty log message ***desmettr
2001-12-07*** empty log message ***desmettr
2001-12-05*** empty log message ***desmettr
2001-12-05*** empty log message ***desmettr
2001-12-05*** empty log message ***desmettr
2001-12-05*** empty log message ***desmettr
2001-12-05*** empty log message ***desmettr
2001-12-05*** empty log message ***desmettr
2001-12-05*** empty log message ***desmettr
2001-12-04Traitement t de -1<>0delahaye
2001-12-04Backtrack sur le commit du 30.11.2001delahaye
2001-12-03*** empty log message ***desmettr
2001-11-30*** empty log message ***desmettr
2001-11-30*** empty log message ***desmettr
2001-11-30*** empty log message ***desmettr
2001-11-30Ajout du fichierdesmettr
2001-11-30Modification de Reals pour integrer les modificationsdesmettr
2001-11-30Ajout du fichier concernant le carre et la racine carreedesmettr
2001-11-30Integration de nouveaux lemmesdesmettr
2001-11-30*** empty log message ***desmettr
2001-11-30Intégration de nouveaux lemmes.desmettr
2001-10-23Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRdelahaye
2001-09-18modif test constmayero
2001-09-11Un look un peu plus avenant aux productions des règles de grammaireherbelin
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-07-19modifs de preuves (plus simples)mayero
2001-06-19Oubli Save + je sais plusmayero
2001-06-18Ajouts de lemmes (pour Float)mayero
2001-06-04Correction bug outsidemayero
2001-05-07ex d'utilisation de fourier avec fieldmayero
2001-04-25coqwebfilliatr
2001-04-24correction nommayero
2001-04-24Ajout de Rseries et Rtrigo_funmayero
2001-04-24(Again) Little corrections for Library doccoq