aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2010-07-16fixed bug #2316 (ring_simplify)barras
2010-07-15Extraction: fix a bit the extraction under modulesletouzey
2010-07-12Fix compilation and test-suite of nsatzglondu
2010-07-08Extraction: restrict autoinling to csts whose body is globally visible (fix #...letouzey
2010-07-08Extraction: more factorization of common match branchesletouzey
2010-07-08Extraction: Unset Extraction AutoInline is now the defaultletouzey
2010-07-08nsatz in an integral domain with specialization to Z and Rpottier
2010-07-07Extraction Library Foo creates Foo.ml, not foo.ml (correct version)letouzey
2010-07-07Extraction Library Foo creates Foo.ml, not foo.mlletouzey
2010-07-07Extraction: get advantage of nicer, algebraic, module typesletouzey
2010-07-07Extraction: some more work on the (re)naming frameworkletouzey
2010-07-05Extraction: (yet another) rework of the renaming codeletouzey
2010-07-02Extraction: better support of modulesletouzey
2010-07-02Extraction: no more MPself hence no need for subst during ppletouzey
2010-06-30Move [delayed] to util and use [force_delayed] everywhere to forcemsozeau
2010-06-30Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.msozeau
2010-06-29QArith: typo in name of hint db (fix #2346)letouzey
2010-06-29change the flag "internal" in declare/ind_tables from bool tovsiles
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-06-28Extraction: handling modules (not functors) in Haskell by name manglingletouzey
2010-06-28Extraction: remove a useless matchletouzey
2010-06-25bug 2328 fixed: failure when polynomial not i idealpottier
2010-06-23Extraction: nicer simple extraction of custom defs (fix #2204)letouzey
2010-06-23Names: remove obsolete mod_self_idletouzey
2010-06-21Extraction: replace unicode characters in ident by ascii encodings (fix #2158...letouzey
2010-06-16Extraction: fix the eta reduction function used in code optimisationsletouzey
2010-06-15Extraction: in support library, more and nicer big_intletouzey
2010-06-14Fixed commit 13125 (stricter check of induction args): an interpretationherbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-06-10Extraction Implicits: can accept argument names instead of just positionsletouzey
2010-06-09Fix bug #2262: bad implicit argument number by avoiding countingmsozeau
2010-06-09Allowing to use an ordering different than Lt with measurejforest
2010-06-08Using vernac parsing for Functionjforest
2010-06-08Extraction with implicits: perform the occur-check after optimisationsletouzey
2010-06-08Made option "Automatic Introduction" active by default before too manyherbelin
2010-06-08Typo in ExtrOcamlString: list char instead of char listletouzey
2010-06-08Fix treatment of {struct x} annotations in presence of generalizedmsozeau
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-06-04Extraction: attempt to provide nice extraction of chars and strings for Ocamlletouzey
2010-06-04Extraction: finish ExtrOcamlNatInt, add similar translation nat==>big_intletouzey
2010-06-03plugins/xml: kill two warningsletouzey
2010-06-03Misc fixes related to new nsatz (and ocamlbuild)letouzey
2010-06-03nsatz ajoutepottier
2010-06-03plugin groebner updated and renamed as nsatz; first version of the doc of nsa...pottier
2010-06-02Fix typosglondu
2010-06-02Extraction: start of a support libraryletouzey
2010-05-28A little bit of cleanup, and some annotations.fkirchne
2010-05-28Modify the test for csdp and associated message.fkirchne
2010-05-28...fkirchne
2010-05-21Extract Inductive is now possible toward non-inductive types (e.g. nat => int)letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 12:30:15 +0000