aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
AgeCommit message (Expand)Author
2010-06-14Fixed commit 13125 (stricter check of induction args): an interpretationherbelin
2010-06-13Fixed a bug in pretty-printing "induction" and "destruct" due to aherbelin
2010-06-09Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.herbelin
2010-06-06Updated performance analysis fileherbelin
2010-05-13Improved the efficiency of evars traverals thanks to a split ofherbelin
2010-04-14Removing redundant internal variants of apply tactic and simplification of ML...herbelin
2010-04-05Added a function in typing.ml to solve evars of a constr w/o going back down ...herbelin
2010-03-04Makefile: cleanup of comments + a few words about recent changes in dev/doc/b...letouzey
2010-01-04Few misc. updates.herbelin
2009-12-13Addition of mergesort + cleaning of the Sorting libraryherbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-08Fixed clash names in Relations (see bug report #2152) and make namesherbelin
2009-08-14Mise à jour du document de révision de la stdlib et déplacement de laherbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-05-24Moved and completed the history of Coq versions from theherbelin
2009-05-09- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceherbelin
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
2009-04-14Correction du patch -rectypes pour ocaml 3.10vsiles
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2009-03-17Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)herbelin
2009-03-14Cleaning/uniformizing the interface of tacticals.mliherbelin
2009-02-17#rectypes was already automatically added when using 3.11herbelin
2009-02-17Made hack to have Drop and #use"include" working with ocaml 3.10 publicherbelin
2009-02-11Document how FIND_VCS_CLAUSE has to be usedlmamane
2009-01-19- Structuring Numbers and fixing Setoid in stdlib's doc.herbelin
2008-12-29- Added support for subterm matching in SearchAbout.herbelin
2008-12-09About "apply in":herbelin
2008-09-06Use $(COQTOPEXE) to refer to bin/coqtop in Makefilesglondu
2008-08-04Évolutions diverses et variées.herbelin
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-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-03Chgts mineurs:herbelin
2008-02-13Implement KEEP_ML4_PREPROCESSED option in build systemlmamane
2008-02-13Implement NO_RECALC_DEPS option in build systemlmamane
2007-10-29MAJherbelin
2007-10-11Allow a few build system optimisations/corner-cuttinglmamane
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:53:01 +0000