| Commit message (Expand) | Author | Age |
|---|
| * | Fixing several bugs with links to notation in coqdoc, including bug #2445: |  herbelin | 2010-12-04 |
| * | Fixing bug using explictly declared implicit arguments in inductive arities. | herbelin | 2010-12-03 |
| * | Redirect stdout to stderr in -ideslave |  glondu | 2010-12-03 |
| * | Remove dead code | glondu | 2010-12-03 |
| * | Fixing a bug introduced in r12304 (move of interpretation of | herbelin | 2010-12-02 |
| * | Document new tactics in CHANGES | glondu | 2010-12-02 |
| * | Documentation for tactic constr_eq | glondu | 2010-12-02 |
| * | Add tactic has_evar (#2433) | glondu | 2010-12-02 |
| * | Add tactic is_evar (Closes: #2433) | glondu | 2010-12-02 |
| * | * Kernel/Term: |  regisgia | 2010-12-01 |
| * | * Kernel/Term | regisgia | 2010-12-01 |
| * | * Kernel/Term | regisgia | 2010-12-01 |
| * | Dp: minor fix suggested by Virgile Prevosto |  letouzey | 2010-11-25 |
| * | CHANGES: mention some changes in trunk since the 8.3 fork | letouzey | 2010-11-19 |
| * | SearchAbout: who has never been annoyed by the [ ] syntax ? | letouzey | 2010-11-19 |
| * | CHANGES: small re-sync with the one of branch v8.3 | letouzey | 2010-11-19 |
| * | adapt slighlty r13642 to support both camlp4 and camlp5-5 and camlp5-6 | letouzey | 2010-11-18 |
| * | Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits | letouzey | 2010-11-18 |
| * | Do not throw an error for anonymous generalized binders as they will be |  msozeau | 2010-11-18 |
| * | NZSqrt: we define sqrt_up, a square root that rounds up instead of down as sqrt | letouzey | 2010-11-18 |
| * | 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 |
herbelin
glondu
regisgia
letouzey
msozeau
jforest
pboutill
soubiran