| Age | Commit message (Expand) | Author |
|---|
| 2010-10-06 | Extraction: allow to use Extraction Inline / NoInline even from under a section. | letouzey |
| 2010-10-06 | Remove unused unshare_proof_tree from xml plugin | glondu |
| 2010-10-06 | Remove open_subgoals field of proof_tree | glondu |
| 2010-10-05 | Auto-inlining of f_terminate in Function | jforest |
| 2010-10-03 | Added multiple implicit arguments rules per name. | herbelin |
| 2010-09-30 | Simplify tactic(_)-bound arguments in TACTIC EXTEND rules | glondu |
| 2010-09-28 | Fix bug #2321, allowing "_" named projections in classes. Not realizing | msozeau |
| 2010-09-28 | Remove some occurrences of "open Termops" | glondu |
| 2010-09-28 | Remove "init" label from Termops.it_mk* specialized functions | glondu |
| 2010-09-24 | Dead code in extraction | letouzey |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-09-21 | Report fix bug 2345 from v8.3 (Bad error message when functional | courtieu |
| 2010-09-20 | Added eta-expansion in kernel, type inference and tactic unification, | herbelin |
| 2010-09-20 | Extraction: re-introduce some eta-expansions in rare situations leading to '_... | letouzey |
| 2010-09-19 | Reverting partial fix for #2335 committed by mistake in r13435. Sorry. | herbelin |
| 2010-09-19 | Patch solving the bug but leaving open design choices | herbelin |
| 2010-09-17 | Extraction: multiple fixes related with the Not_found encountered by X. Leroy | letouzey |
| 2010-09-15 | Fix likely semantic typos | glondu |
| 2010-09-13 | Fix unescaped end-of-lines (OCaml warning 29) | glondu |
| 2010-09-13 | commit 13400 and 13409. | soubiran |
| 2010-09-02 | fixed bug #2375 (congruence) | corbinea |
| 2010-08-02 | Fix [clenv_missing] to compute a better approximation of missing | msozeau |
| 2010-07-28 | unification des tactiques nsatz pour R Z avec celle des anneaux integres | pottier |
| 2010-07-28 | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13338 85f007b7-540e-0... | pottier |
| 2010-07-27 | nstaz pour les anneaux integres et les setoides, R Z et Q | pottier |
| 2010-07-27 | Minor fixes: | msozeau |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-07-23 | correcting a bug in funind introduced in r 13292 | jforest |
| 2010-07-22 | Extension of the recursive notations mechanism | herbelin |
| 2010-07-22 | Simplified the way internalization_data (i.e. bindings of bound vars | herbelin |
| 2010-07-22 | Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt). | herbelin |
| 2010-07-18 | Reverted 13293 commited mistakenly. Sorry for the noise. | herbelin |
| 2010-07-18 | Tentative de suppression de l'import automatique des hints et coercions. | herbelin |
| 2010-07-16 | Amelioration dans Function | jforest |
| 2010-07-16 | fixed bug #2316 (ring_simplify) | barras |
| 2010-07-15 | Extraction: fix a bit the extraction under modules | letouzey |
| 2010-07-12 | Fix compilation and test-suite of nsatz | glondu |
| 2010-07-08 | Extraction: restrict autoinling to csts whose body is globally visible (fix #... | letouzey |
| 2010-07-08 | Extraction: more factorization of common match branches | letouzey |
| 2010-07-08 | Extraction: Unset Extraction AutoInline is now the default | letouzey |
| 2010-07-08 | nsatz in an integral domain with specialization to Z and R | pottier |
| 2010-07-07 | Extraction Library Foo creates Foo.ml, not foo.ml (correct version) | letouzey |
| 2010-07-07 | Extraction Library Foo creates Foo.ml, not foo.ml | letouzey |
| 2010-07-07 | Extraction: get advantage of nicer, algebraic, module types | letouzey |
| 2010-07-07 | Extraction: some more work on the (re)naming framework | letouzey |
| 2010-07-05 | Extraction: (yet another) rework of the renaming code | letouzey |
| 2010-07-02 | Extraction: better support of modules | letouzey |
| 2010-07-02 | Extraction: no more MPself hence no need for subst during pp | letouzey |
| 2010-06-30 | Move [delayed] to util and use [force_delayed] everywhere to force | msozeau |
| 2010-06-30 | Fix (part of) bug #2347, de Bruijn bug in Program's pretyper. | msozeau |
