aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2010-07-29kernel conversion and reduction do not raise assert failure on ill-typed term...barras
2010-07-29test-case for bug #2105barras
2010-07-29fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...barras
2010-07-29fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...barras
2010-07-28Fix bug #2209, don't use the fragile argument name "y" to pass themsozeau
2010-07-28Rewrite Heap merging so that it extracts to an O(n log n) definition.msozeau
2010-07-28unification des tactiques nsatz pour R Z avec celle des anneaux integrespottier
2010-07-28oops. commited files I shouldn't have. reverting on r13341barras
2010-07-28ported r13340 to trunkbarras
2010-07-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 85f007b7-540e-0...pottier
2010-07-28fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodiesbarras
2010-07-27nstaz pour les anneaux integres et les setoides, R Z et Qpottier
2010-07-27Fix computation of fix annotation index: only consider assumptions andmsozeau
2010-07-27Minor fixes:msozeau
2010-07-25Documentation of Set Automatic Coercions Import.herbelin
2010-07-24Fix installation of emacs filesglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-24Updated COPYRIGHT file and header. Improved and fixed header updater.herbelin
2010-07-23correcting a bug in funind introduced in r 13292jforest
2010-07-23Fix a bug found by S.Glondu. coq-db.el did not compile.courtieu
2010-07-23Some fine-tuning after removal of automatic imports of coercions in r13310herbelin
2010-07-22Made notations for exists, exists! and notations of Utf8.v recursive notationsherbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-07-22Simplified the way internalization_data (i.e. bindings of bound varsherbelin
2010-07-22Constrintern: unified push_name_env and push_loc_name_env; madeherbelin
2010-07-22Constrintern: Moved section about binders before section about notationherbelin
2010-07-22Switch to American spelling for "internalise" and "internalisation"herbelin
2010-07-22Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).herbelin
2010-07-22Made coercions active only when modules are imported.herbelin
2010-07-22Backported r13308 (ConstructiveEpsilon.v) to branch v8.3herbelin
2010-07-22Update of ConstructiveEpsilon.v by Jean-François Monin.herbelin
2010-07-22Adding the destauto tactic, that reduces match by destructing matchedcourtieu
2010-07-22ported bug fix r13290 to checkerbarras
2010-07-21Fix for bug #2350 was really too quick. Here is a version that works better.herbelin
2010-07-21Backporting fix to bug #2353 (fixpoint with recursively non-uniformherbelin
2010-07-21Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).herbelin
2010-07-21Applied Pierre Letouzey's patch restoring Convert_concl VM casts in new proofherbelin
2010-07-20Fixed a bug in list_forall2eq (wrong exception was caught).herbelin
2010-07-18Fixed parsing of "Generalizable Variable A" ("Variable" turns to be a keyword).herbelin
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
2010-07-16Amelioration dans Functionjforest
2010-07-16fixed (serious) bug #2353: non-recursive parameters of nested inductive types...barras
2010-07-16removed a potentially dangerous try ... with _ -> ...barras
2010-07-16MSetPositive: mention MSetInterface instead of FSetInterfaceletouzey
2010-07-16FSetPositive: sets of positive inspired by FMapPositive.letouzey
2010-07-16Bool: shorter and more systematic proofs + an iff lemma about eqbletouzey
2010-07-16fixed bug #2316 (ring_simplify)barras
2010-07-15Be more clever when trying to find out the relation inmsozeau
2010-07-15Extraction: fix a bit the extraction under modulesletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 22:09:02 +0000