aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-05-28CyclicAxioms: after discussion with Laurent, znz_WW and variants areletouzey
2008-05-28replace the query window of coqide by a pane in main window as suggested by hugojnarboux
2008-05-28introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...barras
2008-05-28add option to change modifiers of display menujnarboux
2008-05-28update gtk requirementsjnarboux
2008-05-28Réorganisation fenêtre d'accueil CoqIDE et About; nouvelle image deherbelin
2008-05-28add support for pdf in coqdoc, add export to pdf in coqide, port open and sav...jnarboux
2008-05-28debug : case where length of s is < 2...jnarboux
2008-05-28- Correction bug highlighting "Module" dans Coqideherbelin
2008-05-28Cyclic31: proofs for addmuldiv31, tail031 and head031. Only two Admitted left !letouzey
2008-05-27Cyclic31: proof of auxiliary function iter_int31 + (failed) attempt at provin...letouzey
2008-05-27Correction du problème de complexité de Print Assumptions :aspiwack
2008-05-27add install instruction for mandrivajnarboux
2008-05-27Cyclic31: migrate auxiliary lemmas to their legitimate filesletouzey
2008-05-27update changes related to coqidejnarboux
2008-05-27Cyclic31 : proof of the spec of gcd31letouzey
2008-05-27revert toolbar to previous state: icons stylejnarboux
2008-05-26Int31 : gcd31 was wrongletouzey
2008-05-26remove set printing ... and unset printing ... from template menu as they are...jnarboux
2008-05-26Cyclic31: cleanup, 2 Admitted killed (6 remaining)letouzey
2008-05-26transform the toolbar icons for display of information into a Display menu wi...jnarboux
2008-05-26debug subst_command_placeholder : replace %s and not only %jnarboux
2008-05-26Réorganisation des points d'appui du undo de CoqIDE (type reset_info).herbelin
2008-05-26Encore un bug de undoherbelin
2008-05-26Résolution bug #1850 sur notations avec niveaux inconnus deherbelin
2008-05-26Fix bashism in doc generation.glondu
2008-05-26Bug undo CoqIDE sur Endherbelin
2008-05-26the -g option is not recongnized in ocaml < 3.10.0jforest
2008-05-25- Nouvelle option "Set Printing Existential Instances" pour forcerherbelin
2008-05-24- Prise en compte des frozen state de Coq autant que possible pourherbelin
2008-05-24Ajout de la possibilité d'utiliser fix/cofix dans les notations.herbelin
2008-05-23doc of coqchk + improved module cache and computation of module setsbarras
2008-05-23Cyclic31 : replace the ugly time-consuming brute-force proof by a reasonable ...letouzey
2008-05-23- Fix bug #1858, Hint Unfold calling the wrong locate function.msozeau
2008-05-23Nouvelle doc pour les modules.soubiran
2008-05-23(Not completely finished) proofs that int31 integers fulfill the CyclicAxioms...letouzey
2008-05-22Strategy commands are now exportedbarras
2008-05-22fixed dependency problems with the checkerbarras
2008-05-22writing a match on a digit via syntax "if ... then ... else" is not a good id...letouzey
2008-05-22Proposition for a almost-bitsize-independent Int31.v (joint work with J. Voui...letouzey
2008-05-22QRewrite is now obsolete. It was containing manual ltac stuffletouzey
2008-05-22Should fix the dependancy issue mentioned by J.Forest about NMake: letouzey
2008-05-22switch theories/Numbers from Set to Type (both the abstract and the bignum pa...letouzey
2008-05-22improved coqchk targetsbarras
2008-05-22added coqchk to the main Makefile and a make variable VALIDATE to check the v...barras
2008-05-21refined the conversion oraclebarras
2008-05-21refined the conversion oraclebarras
2008-05-21Désactivation affichage image coqide en attendant un barcelosherbelin
2008-05-21Correction bugs ide undo et highlight (suite à typos)herbelin
2008-05-20Correction d'un bug de l'unification pattern qui oubliait d'expanserherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 20:42:20 +0000