aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2010-09-28Remove some occurrences of "open Termops"glondu
2010-09-28Remove "init" label from Termops.it_mk* specialized functionsglondu
2010-09-24Dead code in extractionletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-21Report fix bug 2345 from v8.3 (Bad error message when functionalcourtieu
2010-09-20Added eta-expansion in kernel, type inference and tactic unification,herbelin
2010-09-20Extraction: re-introduce some eta-expansions in rare situations leading to '_...letouzey
2010-09-19Reverting partial fix for #2335 committed by mistake in r13435. Sorry.herbelin
2010-09-19Patch solving the bug but leaving open design choicesherbelin
2010-09-17Extraction: multiple fixes related with the Not_found encountered by X. Leroyletouzey
2010-09-15Fix likely semantic typosglondu
2010-09-13Fix unescaped end-of-lines (OCaml warning 29)glondu
2010-09-13commit 13400 and 13409.soubiran
2010-09-02fixed bug #2375 (congruence)corbinea
2010-08-02Fix [clenv_missing] to compute a better approximation of missingmsozeau
2010-07-28unification des tactiques nsatz pour R Z avec celle des anneaux integrespottier
2010-07-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 85f007b7-540e-0...pottier
2010-07-27nstaz pour les anneaux integres et les setoides, R Z et Qpottier
2010-07-27Minor fixes:msozeau
2010-07-24Updated all headers for 8.3 and trunkherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 04:09:38 +0000