aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
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
2010-05-19Ocamlbuild: various fixletouzey
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19Remove refutpat.ml4, ideal.ml4 is again a normal .ml, let* coded in a naive wayletouzey
2010-05-19static (and shared) camlp4use instead of per-file declarationletouzey
2010-05-19Remove compile-command pragmas for emacsletouzey
2010-05-18Applicative commutative cuts in Fixpoint guard conditionpboutill
2010-05-07better detection of nested recursion in Functionjforest
2010-05-07Correction of a bug pointed by P. Casteran.jforest
2010-05-07Trying to find a problem pointed by P. Casteranjforest
2010-05-04Correction of bug 2290 (removing stupid message)jforest
2010-05-04Correction of bug 2290jforest
2010-05-01Extraction: fix type_expunge_from_sign broken in last commitletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 15:43:22 +0000