aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-04-03- Correction d'un bug de coq_makefile sur les variables CAMLLIBS etnotin
2008-04-03Rework of FMapAVL inspired by recent changes of FSetAVL: letouzey
2008-04-03Chgts mineurs:herbelin
2008-04-03Patch sur le typage d'un foncteur applique a un alias.soubiran
2008-04-02Minor fixes. Use expanded type in class_tactics for Morphism search, tomsozeau
2008-04-02Add the ability to specify the implicit status of section variables andmsozeau
2008-04-01Typo affichage "simple apply"herbelin
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2008-04-01Ajout "simple apply" et "simple eapply" pour apply sans unfoldherbelin
2008-04-01Finish enhancemenent of return clause inference from tycons, integratingmsozeau
2008-04-01Enhance handling of parameters in typeclass constraints: permit to specify an...msozeau
2008-04-01Add option to set the opacity of obligations to transparent, to be ablemsozeau
2008-04-01Correction du bug #1819notin
2008-03-31- Fix for rewriting under dependent products.msozeau
2008-03-30Suite commit 10730: MAJ xlate.mlherbelin
2008-03-30Modifications diverses et variées :herbelin
2008-03-30Ajout d'abbréviations/notations paramétriquesherbelin
2008-03-29Fix test-suite files, change conflicting notation "->rel" and the othersmsozeau
2008-03-28Improve error handling and messages for typeclasses. msozeau
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
2008-03-28Correction du bug 1816 (ajout d'un lemme dans Znat) et suppressionnotin
2008-03-27- notations &&& and ||| equivalent to andb and orb, letouzey
2008-03-27Various fixes on typeclasses:msozeau
2008-03-26Diverses petites modifs dans la test-suite:notin
2008-03-26Bug dans la gestion des dépendances vers les .mlnotin
2008-03-26Correction du bug #1814 (trunk et v8.1) + améliorations dans coqdep et coq_m...notin
2008-03-26Correction d'un bug sur Import/Export : ces fonctionnalites sont gerees en-de...soubiran
2008-03-25Prise en compte des dépendances des .mlnotin
2008-03-25Correction de bugs relatifs a la compostion des substitutionssoubiran
2008-03-25Correction d'un bug dans la gestion des 'Declare ML Module'notin
2008-03-25Interpret patterns for hypotheses types in match goal in type_scope (if not amsozeau
2008-03-24Finish fix in command where we still lost information on what was a typemsozeau
2008-03-23Fix examples in Program documentation and add comindexes for the variousmsozeau
2008-03-23Fix a bug found by B. Grégoire when declaring morphisms in modulemsozeau
2008-03-23Nettoyage Wf.v et unification (suite remarques faites sur cocorico)herbelin
2008-03-23Commit d'une preuve de l'axiome d'Archimède qui traînait dans mes placards.herbelin
2008-03-23Une passe sur les réels:herbelin
2008-03-23CoqIDE default font set to monospace so as indentation to be meaningfulherbelin
2008-03-22Compatibility fixes, backtrack on definitions of reflexive,msozeau
2008-03-21One more AVL reorganisation: separate pure functions from proofs + functional...letouzey
2008-03-21Correct bug introduced in r10589, where we lost information thatmsozeau
2008-03-21Some "if then else" instead of orb and andb, in order to vm_compute lazilyletouzey
2008-03-20Add a flag to control rewriting under lambdas. Otherwise makes somemsozeau
2008-03-20Installation des .vo nécessaire à BigQnotin
2008-03-20Correction d'un bug sur les modules de la forme:soubiran
2008-03-20still some useless invariants in FSetAVLletouzey
2008-03-19some references to IntMap forgotten in last commitletouzey
2008-03-19migration of the old IntMap library from StdLib to a user contrib (Cachan/Int...letouzey
2008-03-19Coq.Relations.Relations can move back to its short nameletouzey
2008-03-19Do another pass on the typeclasses code. Correct globalization of classmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 20:35:51 +0000