aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc
Commit message (Expand)AuthorAge
* Update changelogsGravatar glondu2011-02-11
* Remove obsolete script univdot, update dev doc about universesGravatar glondu2010-12-24
* Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesGravatar glondu2010-09-30
* Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).Gravatar herbelin2010-07-22
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* Fixed commit 13125 (stricter check of induction args): an interpretationGravatar herbelin2010-06-14
* Fixed a bug in pretty-printing "induction" and "destruct" due to aGravatar herbelin2010-06-13
* Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.Gravatar herbelin2010-06-09
* Updated performance analysis fileGravatar herbelin2010-06-06
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* Removing redundant internal variants of apply tactic and simplification of ML...Gravatar herbelin2010-04-14
* Added a function in typing.ml to solve evars of a constr w/o going back down ...Gravatar herbelin2010-04-05
* Makefile: cleanup of comments + a few words about recent changes in dev/doc/b...Gravatar letouzey2010-03-04
* Few misc. updates.Gravatar herbelin2010-01-04
* Addition of mergesort + cleaning of the Sorting libraryGravatar herbelin2009-12-13
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Fixed clash names in Relations (see bug report #2152) and make namesGravatar herbelin2009-10-08
* Mise à jour du document de révision de la stdlib et déplacement de laGravatar herbelin2009-08-14
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Moved and completed the history of Coq versions from theGravatar herbelin2009-05-24
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* Correction du patch -rectypes pour ocaml 3.10Gravatar vsiles2009-04-14
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
* Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)Gravatar herbelin2009-03-17
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* #rectypes was already automatically added when using 3.11Gravatar herbelin2009-02-17
* Made hack to have Drop and #use"include" working with ocaml 3.10 publicGravatar herbelin2009-02-17
* Document how FIND_VCS_CLAUSE has to be usedGravatar lmamane2009-02-11
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* About "apply in":Gravatar herbelin2008-12-09
* Use $(COQTOPEXE) to refer to bin/coqtop in MakefilesGravatar glondu2008-09-06
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* MAJ diversesGravatar herbelin2008-06-11
* - Patch sur "intros until 0"Gravatar herbelin2008-06-08
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Fix typosGravatar lmamane2008-06-05
* - Correction bug highlighting "Module" dans CoqideGravatar herbelin2008-05-28
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* Quelques éléments de réflexionGravatar herbelin2008-05-03
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* Chgts mineurs:Gravatar herbelin2008-04-03
* Implement KEEP_ML4_PREPROCESSED option in build systemGravatar lmamane2008-02-13
* Implement NO_RECALC_DEPS option in build systemGravatar lmamane2008-02-13
* MAJGravatar herbelin2007-10-29
* Allow a few build system optimisations/corner-cuttingGravatar lmamane2007-10-11
* Add glob.dump to Makefile the recommended way and document theGravatar lmamane2007-07-25
* Reorganise cleaning targetsGravatar lmamane2007-07-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 10:28:37 +0000