aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Expand)Author
2009-01-19- Structuring Numbers and fixing Setoid in stdlib's doc.herbelin
2009-01-05Completed 11745 (move of jprover to user contribs) and cleaned 11743herbelin
2008-12-29- Added support for subterm matching in SearchAbout.herbelin
2008-12-09About "apply in":herbelin
2008-11-19Execute #rectypes directive in embedded OCaml toplevel...glondu
2008-11-07- Ajout possibilité de lancer ocamldebug sur coqideherbelin
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2008-09-06Use $(COQTOPEXE) to refer to bin/coqtop in Makefilesglondu
2008-09-02Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutherbelin
2008-08-04Évolutions diverses et variées.herbelin
2008-07-01Various bug fixes in type classes and subtac:msozeau
2008-06-11MAJ diversesherbelin
2008-06-08- Patch sur "intros until 0"herbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-06-06ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...soubiran
2008-06-05Fix typoslmamane
2008-05-28- Correction bug highlighting "Module" dans Coqideherbelin
2008-05-05Mise en place d'un algorithme d'inversion des contraintes de type lorsherbelin
2008-05-03Quelques éléments de réflexionherbelin
2008-04-27Correction du bug des types singletons pas sous-type de Setherbelin
2008-04-24- Add pretty-printers for Idpred, Cpred and transparent_state, used formsozeau
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-16first-order --> firstorder (kills a warning about not being a valid id)letouzey
2008-04-14Diverses corrections herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-03Chgts mineurs:herbelin
2008-03-18Hint for Debian users.glondu
2008-02-13Implement KEEP_ML4_PREPROCESSED option in build systemlmamane
2008-02-13Implement NO_RECALC_DEPS option in build systemlmamane
2008-02-08Add printer for Pp.std_ppcmds...msozeau
2008-01-11Amélioration de la génération des graphes de dépendances (utilisation de ...notin
2008-01-04Prise en compte de CAMLP4LIB via fichier configure plutôt que dynamiquementherbelin
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-07Ocaml toplevel convenience.glondu
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-10-29MAJherbelin
2007-10-11Allow a few build system optimisations/corner-cuttinglmamane
2007-10-08add $COQTOP to the search path of ocamldebugletouzey
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
2007-09-15* Adding compability with ocaml 3.10 + camlp5 (rework of letouzey
2007-08-29- Débogueur: positionnement de set_detype_anonymous pour ne pasherbelin
2007-08-22- Correction bug dans syntaxe des match (liste de motifs vide était acceptée)herbelin
2007-07-25Add glob.dump to Makefile the recommended way and document thelmamane
2007-07-16Reorganise cleaning targetslmamane
2007-07-16A cleaner solution to "make deletes .ml4.d files -> infinite loop" problemlmamane
2007-07-13New bootstrapping, improved, Makefile systemcorbinea
2007-05-21MAJherbelin
2007-04-29Quelques exemples sur l'asymétrie de la conversionherbelin
2007-04-28Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.herbelin
2007-04-18- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771herbelin