aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* * (checker|kernel)/Safe_typing: New LightenLibrary.Gravatar regisgia2010-08-27
* * library/Library: Remove the use of the old-fashioned lighten_library.Gravatar regisgia2010-08-27
* * library/Library: Remove lighten_library definition.Gravatar regisgia2010-08-27
* Fix an error message ot having the ERror: prefix.Gravatar courtieu2010-08-26
* Export printing functions for extra arguments. Maybe there's a way toGravatar msozeau2010-08-03
* Fix [clenv_missing] to compute a better approximation of missingGravatar msozeau2010-08-02
* Fixed commit r13359 which was incomplete for its "trunk" part. ThanksGravatar herbelin2010-07-31
* adpated the checker to handle coomutative cuts and lazynessGravatar barras2010-07-30
* Removed information in COMPATIBILITY that were intended before all forGravatar herbelin2010-07-30
* better fix to bug #2319: types are compiled in the env of the bodiesGravatar barras2010-07-30
* Updated test on Nsatz after Loïc moved NsatzR to Nsatz.Gravatar herbelin2010-07-30
* Capitulation wrt "change pat with term": instead of solving theGravatar herbelin2010-07-30
* r13359 continued: removed native treatment for λ (lambda) and Π (Pi)Gravatar herbelin2010-07-30
* Rather quick hack to make basic unicode notations available byGravatar herbelin2010-07-29
* Fixed a bug introduced (r13316/r13329) in the printing of notationsGravatar herbelin2010-07-29
* kernel conversion and reduction do not raise assert failure on ill-typed term...Gravatar barras2010-07-29
* test-case for bug #2105Gravatar barras2010-07-29
* fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...Gravatar barras2010-07-29
* fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...Gravatar barras2010-07-29
* Fix bug #2209, don't use the fragile argument name "y" to pass theGravatar msozeau2010-07-28
* Rewrite Heap merging so that it extracts to an O(n log n) definition.Gravatar msozeau2010-07-28
* unification des tactiques nsatz pour R Z avec celle des anneaux integresGravatar pottier2010-07-28
* oops. commited files I shouldn't have. reverting on r13341Gravatar barras2010-07-28
* ported r13340 to trunkGravatar barras2010-07-28
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 85f007b7-540e-0...Gravatar pottier2010-07-28
* fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodiesGravatar barras2010-07-28
* nstaz pour les anneaux integres et les setoides, R Z et QGravatar pottier2010-07-27
* Fix computation of fix annotation index: only consider assumptions andGravatar msozeau2010-07-27
* Minor fixes:Gravatar msozeau2010-07-27
* Documentation of Set Automatic Coercions Import.Gravatar herbelin2010-07-25
* Fix installation of emacs filesGravatar glondu2010-07-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Updated COPYRIGHT file and header. Improved and fixed header updater.Gravatar herbelin2010-07-24
* correcting a bug in funind introduced in r 13292Gravatar jforest2010-07-23
* Fix a bug found by S.Glondu. coq-db.el did not compile.Gravatar courtieu2010-07-23
* Some fine-tuning after removal of automatic imports of coercions in r13310Gravatar herbelin2010-07-23
* Made notations for exists, exists! and notations of Utf8.v recursive notationsGravatar herbelin2010-07-22
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Simplified the way internalization_data (i.e. bindings of bound varsGravatar herbelin2010-07-22
* Constrintern: unified push_name_env and push_loc_name_env; madeGravatar herbelin2010-07-22
* Constrintern: Moved section about binders before section about notationGravatar herbelin2010-07-22
* Switch to American spelling for "internalise" and "internalisation"Gravatar herbelin2010-07-22
* Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).Gravatar herbelin2010-07-22
* Made coercions active only when modules are imported.Gravatar herbelin2010-07-22
* Backported r13308 (ConstructiveEpsilon.v) to branch v8.3Gravatar herbelin2010-07-22
* Update of ConstructiveEpsilon.v by Jean-François Monin.Gravatar herbelin2010-07-22
* Adding the destauto tactic, that reduces match by destructing matchedGravatar courtieu2010-07-22
* ported bug fix r13290 to checkerGravatar barras2010-07-22
* Fix for bug #2350 was really too quick. Here is a version that works better.Gravatar herbelin2010-07-21
* Backporting fix to bug #2353 (fixpoint with recursively non-uniformGravatar herbelin2010-07-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 02:37:20 +0000