aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* 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
* Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).Gravatar herbelin2010-07-21
* Applied Pierre Letouzey's patch restoring Convert_concl VM casts in new proofGravatar herbelin2010-07-21
* Fixed a bug in list_forall2eq (wrong exception was caught).Gravatar herbelin2010-07-20
* Fixed parsing of "Generalizable Variable A" ("Variable" turns to be a keyword).Gravatar herbelin2010-07-18
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* Amelioration dans FunctionGravatar jforest2010-07-16
* fixed (serious) bug #2353: non-recursive parameters of nested inductive types...Gravatar barras2010-07-16
* removed a potentially dangerous try ... with _ -> ...Gravatar barras2010-07-16
* MSetPositive: mention MSetInterface instead of FSetInterfaceGravatar letouzey2010-07-16
* FSetPositive: sets of positive inspired by FMapPositive.Gravatar letouzey2010-07-16
* Bool: shorter and more systematic proofs + an iff lemma about eqbGravatar letouzey2010-07-16
* fixed bug #2316 (ring_simplify)Gravatar barras2010-07-16
* Be more clever when trying to find out the relation inGravatar msozeau2010-07-15
* Extraction: fix a bit the extraction under modulesGravatar letouzey2010-07-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 19:36:06 +0000