| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | Restored checking that _all_ arguments of the command line are meaningful |  herbelin | 2010-11-01 |
| * | Add tolerance for existential variables in Check. | herbelin | 2010-10-31 |
| * | An experimental support for open constrs in hints and in "using" | herbelin | 2010-10-31 |
| * | Cleaning the use of parentheses around evd and evdref (cosmetic commit). | herbelin | 2010-10-31 |
| * | Minor code improvements around libobject | herbelin | 2010-10-31 |
| * | Minor factorization of the part of the code used for Unnamed_thm saving. | herbelin | 2010-10-31 |
| * | Slight code cleaning in auto.ml (made code of make_exact_entry and | herbelin | 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-31 |
| * | correction of bug #2414 (report of r 13586) |  jforest | 2010-10-27 |
| * | Compatibility camlp4/camlp5 | herbelin | 2010-10-26 |
| * | Fail, when successful, prints something only in verbose mode | glondu | 2010-10-26 |
| * | Fix minor typo in error message (Closes: #2408) | glondu | 2010-10-25 |
| * | 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-23 |
| * | FMapFacts: typo noticed by Aaron |  letouzey | 2010-10-22 |
| * | Still another Open Scope than should be Local | letouzey | 2010-10-22 |
| * | 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-21 |
| * | Oups, new file Zsqrt_def was exporting Z_scope | letouzey | 2010-10-20 |
| * | Numbers: no need for advanced functions (e.g. sqrt) in NStrongRec, NDefOps, etc | letouzey | 2010-10-19 |
| * | Add sqrt in Numbers | letouzey | 2010-10-19 |
| * | About "unsupported" unicode characters in notations. | herbelin | 2010-10-17 |
| * | Fix missing -coqlib argument to coqdep in test-suite | glondu | 2010-10-16 |
| * | Support for GNU Make 3.82 | glondu | 2010-10-16 |
| * | 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-14 |
| * | 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-12 |
| * | 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-11 |
| * | Export the "bullet" grammar entry | glondu | 2010-10-08 |
| * | update CHANGES w.r.t. extraction | letouzey | 2010-10-08 |
| * | 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-07 |
| * | 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 |
herbelin
glondu
jforest
letouzey
msozeau
vgross