aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Expand)AuthorAge
* Remove useless ppevd (which is identical to ppevm)Gravatar glondu2009-11-13
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Fixed bug #2168 (closing a section may have as side-effect the erasureGravatar herbelin2009-11-11
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Fixed "Scheme Equality" when another instance of the scheme on theGravatar herbelin2009-11-08
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Fixed clash names in Relations (see bug report #2152) and make namesGravatar herbelin2009-10-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Mise à jour du document de révision de la stdlib et déplacement de laGravatar herbelin2009-08-14
* Fixed incorrect optimization in Prettyp.pr_located_qualid introducedGravatar herbelin2009-08-07
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* ocamldebug-coq: add some forgotten -IGravatar letouzey2009-05-26
* Moved and completed the history of Coq versions from theGravatar herbelin2009-05-24
* - Fixing declarative mode in presence of high use of Change_evars nodesGravatar herbelin2009-05-20
* - 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
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
* Correction du patch -rectypes pour ocaml 3.10Gravatar vsiles2009-04-14
* Complementary fix to have ocamlopt_shared_os5fix.sh working correctlyGravatar herbelin2009-03-31
* Fix the fix script for ocamlopt -shared in MacOS 10.5 (remarks by Hugo)Gravatar letouzey2009-03-30
* ocamlbuild: many improvements (macos 10.5 fix, correct dllpath, etc)Gravatar letouzey2009-03-29
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
* 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
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* #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
* Completed 11745 (move of jprover to user contribs) and cleaned 11743Gravatar herbelin2009-01-05
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* About "apply in":Gravatar herbelin2008-12-09
* Execute #rectypes directive in embedded OCaml toplevel...Gravatar glondu2008-11-19
* - Ajout possibilité de lancer ocamldebug sur coqideGravatar herbelin2008-11-07
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* Use $(COQTOPEXE) to refer to bin/coqtop in MakefilesGravatar glondu2008-09-06
* Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutGravatar herbelin2008-09-02
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Various bug fixes in type classes and subtac:Gravatar msozeau2008-07-01
* 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
* ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...Gravatar soubiran2008-06-06
* Fix typosGravatar lmamane2008-06-05
* - Correction bug highlighting "Module" dans CoqideGravatar herbelin2008-05-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 16:38:36 +0000