aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-05-23git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0...fbesson
2011-05-23ported r14149 from v8.3 branch: bug in checker (redefined global)barras
2011-05-21Restore display of notation when printing an inductive such as sigletouzey
2011-05-20added support to handle division by a constant over Rfbesson
2011-05-19Remove useless "open Gc"glondu
2011-05-19Remove System.process_time (dead code)glondu
2011-05-19Extraction: avoid lots of late mind_of_knletouzey
2011-05-19Extraction: global reference should be indexed on their user part (fix #2540)letouzey
2011-05-18cbv delta - [...] before calling liafbesson
2011-05-18apply zeta reduction before syntaxificationfbesson
2011-05-18Extraction: avoid printing of Recursive Extraction in coqide's consoleletouzey
2011-05-18Coqide: allow the use of Abort (grant wish #2357)letouzey
2011-05-17Class_tactics: Pervasives.(=) don't work for named_context_val (fix ATBR)letouzey
2011-05-17Modops: the strengthening functions can work without any env argumentletouzey
2011-05-17More work on error handlingletouzey
2011-05-17Add simple test of bullet behaviour.aspiwack
2011-05-17Break circular dependency Proof_global -> Vernacexpr -> Proof_global.aspiwack
2011-05-17Fixes bug in [maximal_unfocus] introduced in r14120.aspiwack
2011-05-16Repair the "Fail" command after recent changes in exception handlingletouzey
2011-05-16test-suite: no more ..._beq in the output of the search testsletouzey
2011-05-16Fix order in Search tests.letouzey
2011-05-16Fixed my last patch: these files no longer use nat_beq (automaticallyvsiles
2011-05-16turn the automatic generation of boolean equalityvsiles
2011-05-15Test for bug 462 and 2342 fixed by Matthieu's 13990 (or so).herbelin
2011-05-15Failing instead of switching to the coercion mechanism when VMcastherbelin
2011-05-15Turning Sys_error into error by default instead of anomaly. After all,herbelin
2011-05-13A better procedure for checking presence of undefined evars.aspiwack
2011-05-13The modules in proofs now use the Errors module to explain their exceptions t...aspiwack
2011-05-13A new mechanism to handle errors.aspiwack
2011-05-13New option [Set Bullet Behavior] allows to select the behaviour of bullets.aspiwack
2011-05-11Print Module (Type) M now tries to print more detailsletouzey
2011-05-09Improved lia + experimental nliafbesson
2011-05-09remove useless dependancy for csdpcertfbesson
2011-05-06Fixes in the test-suite after modularisation of ZArith and coletouzey
2011-05-06Additionnal fix of romega after modularisation of ZArithletouzey
2011-05-06update of the file list in doc/stdlibletouzey
2011-05-05BinNat: N.binary_rect is now a definition instead of an opaque proofletouzey
2011-05-05Peano recursion for positive: integration of Daniel Schepler's codeletouzey
2011-05-05Minimal lemmas about Z.gt, N.gt and coletouzey
2011-05-05Modularisation of Znat, a few name changed elsewhereletouzey
2011-05-05BinInt: Z.add become the alternative Z.add'letouzey
2011-05-05Modularization of BinInt, related fixes in the stdlibletouzey
2011-05-05Modularization of Nnatletouzey
2011-05-05Setoid_ring: some cleanups related with BinPos and BinNatletouzey
2011-05-05Wf.iter_nat becomes Peano.nat_iter (with an implicit arg)letouzey
2011-05-05BinNatDef containing all functions of BinNat, misc adaptations in BinPosletouzey
2011-05-05BinPosDef: a module with all code about positive, later Included in BinPosletouzey
2011-05-05Modularization of BinNat + fixes of stdlibletouzey
2011-05-05Modularization of Pnatletouzey
2011-05-05Modularization of BinPos + fixes in Stdlibletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 19:36:33 +0000