| Age | Commit message (Expand) | Author |
|---|
| 2010-11-04 | Fixing a regression wrt 8.2 when using an "ident" several times in a notation | herbelin |
| 2010-11-03 | Fix typo in "Hint Extern" doc | glondu |
| 2010-11-03 | Correction bug 2427 | soubiran |
| 2010-11-03 | Remove suspiciously named "implicit" stuff from Term | glondu |
| 2010-11-03 | In Univ, unify order_request and constraint_type | glondu |
| 2010-11-02 | Add small utility lemmas about nat/P/Z/Q arithmetic. | letouzey |
| 2010-11-02 | Document DOT output of universe graph | glondu |
| 2010-11-02 | Output universe graph in DOT language if output file ends in .dot or .gv | glondu |
| 2010-11-02 | More generic Univ.dump_universes | glondu |
| 2010-11-02 | NZSqrt : since spec is complete, no need for morphism axiom sqrt_wd | letouzey |
| 2010-11-02 | NZLog : since spec is complete, no need for morphism axiom log2_wd | letouzey |
| 2010-11-02 | Numbers: misc improvements | letouzey |
| 2010-11-02 | Numbers : log2. Abstraction, properties and implementations. | letouzey |
| 2010-11-02 | NArith: a log2 function | letouzey |
| 2010-11-02 | NPeano: A log2 function for nat | letouzey |
| 2010-11-02 | Numbers: specs about sqrt and pow of neg numbers, even in NZ | letouzey |
| 2010-11-02 | Numbers: NZPowProp as a Module Type, some module variable renaming | letouzey |
| 2010-11-02 | Move stuff about positive into a distinct PArith subdir | letouzey |
| 2010-11-01 | Restored checking that _all_ arguments of the command line are meaningful | herbelin |
| 2010-10-31 | 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-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 |
