aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
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
2011-02-25Extraction: Add missing parenthesis around emulated pattern-match (fix #2478)letouzey
2011-02-25Fix indentation of default pattern in haskell case (bug #2476)letouzey
2011-02-25Revert "syntax for exponents"glondu
2011-02-22syntax for exponentspottier
2011-02-22anneaux commutatifs ou non, reification sans mlpottier
2011-02-10Interp a definition with the implicit arguments of its local contextpboutill
2011-02-10Data structure telling implicits of local variables is a map in thepboutill
2011-02-10Started to fix the declarative proof mode (C-zar).aspiwack
2011-02-03Dp: another fix suggested by Virgile Prevostoletouzey
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2011-01-07Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)letouzey
2010-12-25ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPEDglondu
2010-12-25Rename mkR* smart constructors (mostly in funind)glondu
2010-12-24s/raw/glob/g in decl_interp.ml for more consistencyglondu
2010-12-24More {raw => glob} changes for consistencyglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 15:51:18 +0000