aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2011-06-30Fix compilation errormsozeau
2011-06-30Keep obligation source information in Programmsozeau
2011-06-29update of Micromega docfbesson
2011-06-28Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_defletouzey
2011-06-28improved tactic namesfbesson
2011-06-24Numbers: a particular case of div_uniqueletouzey
2011-06-21Follow-up concerning eqb / ltb / leb comparisonsletouzey
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
2011-06-17Fix bug 2269, program typechecker not used in Instance conclusionsmsozeau
2011-06-16Tests de nsatz avec la geometriepottier
2011-06-10Moved allow_K to a unification flagherbelin
2011-06-10Call process_vernac_interp_error before calling Errors.print inherbelin
2011-06-10Revert "Check if recursive calls are guarded before printing "Proof completed"."pboutill
2011-06-10ring2, cring, nsatz avec type classe avec parametres plus notationspottier
2011-06-07Fix bug #2399 in Program: used to build an ill-formed term due to a de Bruijn...msozeau
2011-06-07Fix bug #2415: warn when closing modules or sections and some obligations are...msozeau
2011-05-26Check if recursive calls are guarded before printing "Proof completed".herbelin
2011-05-25Q2R -> IQRfbesson
2011-05-24Made the emacs-U option deprecated. Also removed the old codecourtieu
2011-05-23git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0...fbesson
2011-05-20added support to handle division by a constant over Rfbesson
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-16Fixed my last patch: these files no longer use nat_beq (automaticallyvsiles
2011-05-13A new mechanism to handle errors.aspiwack
2011-05-11Print Module (Type) M now tries to print more detailsletouzey
2011-05-09Improved lia + experimental nliafbesson
2011-05-06Additionnal fix of romega after modularisation of ZArithletouzey
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-05Setoid_ring: some cleanups related with BinPos and BinNatletouzey
2011-05-05Modularization of BinNat + fixes of stdlibletouzey
2011-05-05Modularization of Pnatletouzey
2011-05-05Modularization of BinPos + fixes in Stdlibletouzey
2011-05-05Definitions of positive, N, Z moved in Numbers/BinNums.vletouzey
2011-05-05Extraction: allow extraction foo when foo is an alias notationletouzey
2011-05-04First phase removing obsolete support for eta up to conversion inherbelin
2011-04-29Fixed a bug causing inconsistent states during proof editting.aspiwack
2011-04-21bug fix: concurrent access of persistent_cachefbesson
2011-04-19Declarative mode: fix escape and return.aspiwack
2011-04-15Extraction: nicer error when a toplevel module has no body (#2525)letouzey
2011-04-15Extraction: allow extracting Ascii.ascii to native Char in Haskell (fix #2515)letouzey
2011-04-13Extraction: opaque terms are not traversed anymore by defaultletouzey
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 22:13:30 +0000