| Commit message (Expand) | Author | Age |
* | NZLog: we define log2_up, a base-2 logarithm that rounds up instead of down a... | letouzey | 2010-11-18 |
* | Support for camlp5 6.02.0 (Closes: #2432) | glondu | 2010-11-16 |
* | Division: avoid imposing rem as an infix keyword in Z_scope and bigZ_scope. | letouzey | 2010-11-16 |
* | Remove redundant clause (and fix compatibility issue) | glondu | 2010-11-16 |
* | Use full path for unknown stuff in omega | glondu | 2010-11-16 |
* | Minor fixes from Gregory Malecha. A typo fixed and a better (located) | msozeau | 2010-11-15 |
* | Oups, fix last commit, a missing file in a vo.itarget | letouzey | 2010-11-10 |
* | Integer division: quot and rem (trunc convention) in addition to div and mod | letouzey | 2010-11-10 |
* | Refresh universes in params when generating schemes (Closes: #2429) | glondu | 2010-11-08 |
* | Print universes in debugging printers | glondu | 2010-11-08 |
* | Delayed the evar normalization in error messages to the last minute | herbelin | 2010-11-07 |
* | Improved error messages in CoqIDE: | herbelin | 2010-11-07 |
* | Add information of localisation when an error involving an "implicit | herbelin | 2010-11-07 |
* | correcting a non catch error reported as an anomaly (Ploc.Exc) | jforest | 2010-11-07 |
* | Numbers: axiomatization, properties and implementations of gcd | letouzey | 2010-11-05 |
* | End of commit 13600: files can be given as arguments of coqide again. | pboutill | 2010-11-04 |
* | Fixing a regression wrt 8.2 when using an "ident" several times in a notation | herbelin | 2010-11-04 |
* | 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-03 |
* | 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-02 |
* | 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 |