aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* add support for pdf in coqdoc, add export to pdf in coqide, port open and sav...Gravatar jnarboux2008-05-28
* debug : case where length of s is < 2...Gravatar jnarboux2008-05-28
* - Correction bug highlighting "Module" dans CoqideGravatar herbelin2008-05-28
* Cyclic31: proofs for addmuldiv31, tail031 and head031. Only two Admitted left !Gravatar letouzey2008-05-28
* Cyclic31: proof of auxiliary function iter_int31 + (failed) attempt at provin...Gravatar letouzey2008-05-27
* Correction du problème de complexité de Print Assumptions :Gravatar aspiwack2008-05-27
* add install instruction for mandrivaGravatar jnarboux2008-05-27
* Cyclic31: migrate auxiliary lemmas to their legitimate filesGravatar letouzey2008-05-27
* update changes related to coqideGravatar jnarboux2008-05-27
* Cyclic31 : proof of the spec of gcd31Gravatar letouzey2008-05-27
* revert toolbar to previous state: icons styleGravatar jnarboux2008-05-27
* Int31 : gcd31 was wrongGravatar letouzey2008-05-26
* remove set printing ... and unset printing ... from template menu as they are...Gravatar jnarboux2008-05-26
* Cyclic31: cleanup, 2 Admitted killed (6 remaining)Gravatar letouzey2008-05-26
* transform the toolbar icons for display of information into a Display menu wi...Gravatar jnarboux2008-05-26
* debug subst_command_placeholder : replace %s and not only %Gravatar jnarboux2008-05-26
* Réorganisation des points d'appui du undo de CoqIDE (type reset_info).Gravatar herbelin2008-05-26
* Encore un bug de undoGravatar herbelin2008-05-26
* Résolution bug #1850 sur notations avec niveaux inconnus deGravatar herbelin2008-05-26
* Fix bashism in doc generation.Gravatar glondu2008-05-26
* Bug undo CoqIDE sur EndGravatar herbelin2008-05-26
* the -g option is not recongnized in ocaml < 3.10.0Gravatar jforest2008-05-26
* - Nouvelle option "Set Printing Existential Instances" pour forcerGravatar herbelin2008-05-25
* - Prise en compte des frozen state de Coq autant que possible pourGravatar herbelin2008-05-24
* Ajout de la possibilité d'utiliser fix/cofix dans les notations.Gravatar herbelin2008-05-24
* doc of coqchk + improved module cache and computation of module setsGravatar barras2008-05-23
* Cyclic31 : replace the ugly time-consuming brute-force proof by a reasonable ...Gravatar letouzey2008-05-23
* - Fix bug #1858, Hint Unfold calling the wrong locate function.Gravatar msozeau2008-05-23
* Nouvelle doc pour les modules.Gravatar soubiran2008-05-23
* (Not completely finished) proofs that int31 integers fulfill the CyclicAxioms...Gravatar letouzey2008-05-23
* Strategy commands are now exportedGravatar barras2008-05-22
* fixed dependency problems with the checkerGravatar barras2008-05-22
* writing a match on a digit via syntax "if ... then ... else" is not a good id...Gravatar letouzey2008-05-22
* Proposition for a almost-bitsize-independent Int31.v (joint work with J. Voui...Gravatar letouzey2008-05-22
* QRewrite is now obsolete. It was containing manual ltac stuffGravatar letouzey2008-05-22
* Should fix the dependancy issue mentioned by J.Forest about NMake: Gravatar letouzey2008-05-22
* switch theories/Numbers from Set to Type (both the abstract and the bignum pa...Gravatar letouzey2008-05-22
* improved coqchk targetsGravatar barras2008-05-22
* added coqchk to the main Makefile and a make variable VALIDATE to check the v...Gravatar barras2008-05-22
* refined the conversion oracleGravatar barras2008-05-21
* refined the conversion oracleGravatar barras2008-05-21
* Désactivation affichage image coqide en attendant un barcelosGravatar herbelin2008-05-21
* Correction bugs ide undo et highlight (suite à typos)Gravatar herbelin2008-05-21
* Correction d'un bug de l'unification pattern qui oubliait d'expanserGravatar herbelin2008-05-20
* Corrections d'erreurs rapportées par Frédéric Besson sur le précédentGravatar herbelin2008-05-20
* added checker to svn:ignoreGravatar barras2008-05-20
* also fixed conversion of the checkerGravatar barras2008-05-20
* Cleanup build_new, remove unneeded try-with and debug interaction ofGravatar msozeau2008-05-20
* Léger backtrack sur commit coqide précédent (si la commande à annulerGravatar herbelin2008-05-20
* Fixed coqide bug #1856 that was introduced in revision 10915.Gravatar herbelin2008-05-20