| Age | Commit message (Expand) | Author |
|---|
| 2010-10-31 | Slight cosmetic cleaning of tacred.ml. | herbelin |
| 2010-10-31 | Add (quilt's) .pc to .gitignore | glondu |
| 2010-10-31 | Remove some unnecessary (?) "open Ideutils" | glondu |
| 2010-10-31 | Remove (unused) ide/highlight.mll | glondu |
| 2010-10-27 | correction of bug #2414 (report of r 13586) | jforest |
| 2010-10-26 | Compatibility camlp4/camlp5 | herbelin |
| 2010-10-26 | Fail, when successful, prints something only in verbose mode | glondu |
| 2010-10-25 | Fix minor typo in error message (Closes: #2408) | glondu |
| 2010-10-23 | Fixing bug #2412, continued (preprocessing of Ltac Debug errors | herbelin |
| 2010-10-23 | Used multiple lists of implicit arguments to transfer the choices of | herbelin |
| 2010-10-23 | Automatically translate hints of the form "c _ ... _" into "c". Besides | herbelin |
| 2010-10-23 | Fixing bug #2412 (preprocessing of Ltac Debug errors forgotten in r13431). | herbelin |
| 2010-10-22 | FMapFacts: typo noticed by Aaron | letouzey |
| 2010-10-22 | Still another Open Scope than should be Local | letouzey |
| 2010-10-21 | Solve name conflict about pow introduced by commit 13546. | letouzey |
| 2010-10-21 | Still some more Cpow in Type rather than Set (cf. r13542) | letouzey |
| 2010-10-20 | Oups, new file Zsqrt_def was exporting Z_scope | letouzey |
| 2010-10-19 | Numbers: no need for advanced functions (e.g. sqrt) in NStrongRec, NDefOps, etc | letouzey |
| 2010-10-19 | Add sqrt in Numbers | letouzey |
| 2010-10-17 | About "unsupported" unicode characters in notations. | herbelin |
| 2010-10-16 | Fix missing -coqlib argument to coqdep in test-suite | glondu |
| 2010-10-16 | Support for GNU Make 3.82 | glondu |
| 2010-10-14 | Numbers : also axiomatize constants 1 and 2. | letouzey |
| 2010-10-14 | Reparation du parseur/printer de nombres BigN | letouzey |
| 2010-10-14 | Numbers: new functions pow, even, odd + many reorganisations | letouzey |
| 2010-10-14 | Zeven: some complements, e.g. proofs that Zeven_bool and co are ok | letouzey |
| 2010-10-14 | NArith: add some functions Neven and Nodd | letouzey |
| 2010-10-14 | NArith: Definition of a Npow power function | letouzey |
| 2010-10-14 | Ring : Cpow in Type rather than Set (type of power coeffs in power_theory) | letouzey |
| 2010-10-12 | Adding test-case for bug #2362, which uses HO unification during | msozeau |
| 2010-10-12 | Fix bug #2393: allow let-ins inside telescopes (only fails when there's | msozeau |
| 2010-10-11 | Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, looping | herbelin |
| 2010-10-11 | More precise description of boolean ring in doc (see bug #2401) | glondu |
| 2010-10-08 | Export the "bullet" grammar entry | glondu |
| 2010-10-08 | update CHANGES w.r.t. extraction | letouzey |
| 2010-10-07 | Fix bug# 2392 | msozeau |
| 2010-10-07 | TeX input method is now supported upstream | vgross |
| 2010-10-07 | test-suite: fix success/unification.v | glondu |
| 2010-10-06 | Fixing the Not_found error in bug #2404 + dead code removal in cases.ml | herbelin |
| 2010-10-06 | Remove Explain* vernacs | glondu |
| 2010-10-06 | Extraction: allow to use Extraction Inline / NoInline even from under a section. | letouzey |
| 2010-10-06 | test-suite: fix output/Existentials.out | glondu |
| 2010-10-06 | Remove ide/coq_tactics.ml* | glondu |
| 2010-10-06 | Remove VernacGo | glondu |
| 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 | (Hopefully) clearer explanation of Ltac's context patterns | glondu |
| 2010-10-05 | test-suite: fix success/Typeclasses.v | glondu |
| 2010-10-05 | test-suite: fix success/AdvancedCanonicalStructure.v | glondu |
| 2010-10-05 | Export definition of type implicits_list for contribs + fixed a | herbelin |
