aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Fix [clenv_missing] to compute a better approximation of missingGravatar msozeau2010-08-02
* unification des tactiques nsatz pour R Z avec celle des anneaux integresGravatar pottier2010-07-28
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 85f007b7-540e-0...Gravatar pottier2010-07-28
* nstaz pour les anneaux integres et les setoides, R Z et QGravatar pottier2010-07-27
* Minor fixes:Gravatar msozeau2010-07-27
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* correcting a bug in funind introduced in r 13292Gravatar jforest2010-07-23
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Simplified the way internalization_data (i.e. bindings of bound varsGravatar herbelin2010-07-22
* Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).Gravatar herbelin2010-07-22
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* Amelioration dans FunctionGravatar jforest2010-07-16
* fixed bug #2316 (ring_simplify)Gravatar barras2010-07-16
* Extraction: fix a bit the extraction under modulesGravatar letouzey2010-07-15
* Fix compilation and test-suite of nsatzGravatar glondu2010-07-12
* Extraction: restrict autoinling to csts whose body is globally visible (fix #...Gravatar letouzey2010-07-08
* Extraction: more factorization of common match branchesGravatar letouzey2010-07-08
* Extraction: Unset Extraction AutoInline is now the defaultGravatar letouzey2010-07-08
* nsatz in an integral domain with specialization to Z and RGravatar pottier2010-07-08
* Extraction Library Foo creates Foo.ml, not foo.ml (correct version)Gravatar letouzey2010-07-07
* Extraction Library Foo creates Foo.ml, not foo.mlGravatar letouzey2010-07-07
* Extraction: get advantage of nicer, algebraic, module typesGravatar letouzey2010-07-07
* Extraction: some more work on the (re)naming frameworkGravatar letouzey2010-07-07
* Extraction: (yet another) rework of the renaming codeGravatar letouzey2010-07-05
* Extraction: better support of modulesGravatar letouzey2010-07-02
* Extraction: no more MPself hence no need for subst during ppGravatar letouzey2010-07-02
* Move [delayed] to util and use [force_delayed] everywhere to forceGravatar msozeau2010-06-30
* Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.Gravatar msozeau2010-06-30
* QArith: typo in name of hint db (fix #2346)Gravatar letouzey2010-06-29
* change the flag "internal" in declare/ind_tables from bool toGravatar vsiles2010-06-29
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* Extraction: handling modules (not functors) in Haskell by name manglingGravatar letouzey2010-06-28
* Extraction: remove a useless matchGravatar letouzey2010-06-28
* bug 2328 fixed: failure when polynomial not i idealGravatar pottier2010-06-25
* Extraction: nicer simple extraction of custom defs (fix #2204)Gravatar letouzey2010-06-23
* Names: remove obsolete mod_self_idGravatar letouzey2010-06-23
* Extraction: replace unicode characters in ident by ascii encodings (fix #2158...Gravatar letouzey2010-06-21
* Extraction: fix the eta reduction function used in code optimisationsGravatar letouzey2010-06-16
* Extraction: in support library, more and nicer big_intGravatar letouzey2010-06-15
* Fixed commit 13125 (stricter check of induction args): an interpretationGravatar herbelin2010-06-14
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Extraction Implicits: can accept argument names instead of just positionsGravatar letouzey2010-06-10
* Fix bug #2262: bad implicit argument number by avoiding countingGravatar msozeau2010-06-09
* Allowing to use an ordering different than Lt with measureGravatar jforest2010-06-09
* Using vernac parsing for FunctionGravatar jforest2010-06-08
* Extraction with implicits: perform the occur-check after optimisationsGravatar letouzey2010-06-08
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Typo in ExtrOcamlString: list char instead of char listGravatar letouzey2010-06-08
* Fix treatment of {struct x} annotations in presence of generalizedGravatar msozeau2010-06-08