aboutsummaryrefslogtreecommitdiff
path: root/plugins
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-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
2011-04-08Replaced printing number of ill-typed branch by printing name of constructorherbelin
2011-04-07Extraction: unfolds the let-in created by Program when handling "match"letouzey
2011-04-07Extraction: avoid some useless Obj.magic by fixing my ML type unifierletouzey
2011-04-06Fixes the weird bug of the declarative proof mode (Czar) both in emacs and coqc.aspiwack
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-04-03Quickly avoid global axioms in Loic new files about ringletouzey
2011-03-31Extraction: customized inductives are always standardglondu
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-03-11Keep information on which fields are subclasses in class declarations,msozeau
2011-03-11Tentative to make unification check types at every instanciation of anmsozeau
2011-03-08syntax for exponentspottier
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
2011-03-07Extraction: a warning when an opaque constant is enterredletouzey
2011-03-07Extraction: fix printing of haskell modular namesletouzey
2011-03-07Extraction: avoid printing unused mutual fix components (fix #2477)letouzey
2011-03-07A new command "Separate Extraction"letouzey
2011-03-05Improved define_evar_as_lambda which was creating an unrelated new evarherbelin
2011-03-04Extraction: improved indentation of extracted code (fix #2497)letouzey
2011-02-28Add a flag to hide obligations in Program-generated terms under anmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 02:57:31 +0000