aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2010-07-23correcting a bug in funind introduced in r 13292jforest
2010-07-22Extension of the recursive notations mechanismherbelin
2010-07-22Simplified the way internalization_data (i.e. bindings of bound varsherbelin
2010-07-22Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).herbelin
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
2010-07-16Amelioration dans Functionjforest
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 10:19:39 +0000