| Commit message (Expand) | Author | Age |
* | Patch on subtyping check of opaque constants. | soubiran | 2010-01-06 |
* | "by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... ... | letouzey | 2010-01-06 |
* | Numbers abstract layer: more Module Type, used especially for divisions. | letouzey | 2010-01-05 |
* | Avoid declaring hints about refl/sym/trans of eq in DecidableType2 | letouzey | 2010-01-05 |
* | Division in Numbers: proofs with less auto (less sensitive to hints, in parti... | letouzey | 2010-01-05 |
* | Division in Numbers: factorisation of signatures | letouzey | 2010-01-05 |
* | Specific syntax for Instances in Module Type: Declare Instance | letouzey | 2010-01-04 |
* | RelationPairs: stop loading it in all Numbers, stop maximal args with fst/snd | letouzey | 2009-12-18 |
* | Division in Numbers : more properties, new filenames based on a paper by R. B... | letouzey | 2009-12-17 |
* | Division in Numbers: more properties proved (still W.I.P.) | letouzey | 2009-12-16 |
* | A generic euclidean division in Numbers (Still Work-In-Progress) | letouzey | 2009-12-15 |
* | NZDomain: investigation of the shape of NZ domain, more results about ofnat:n... | letouzey | 2009-12-10 |
* | Factorisation between Makefile and ocamlbuild systems : .vo to compile are in... | letouzey | 2009-12-09 |
* | Forgot a file in last commit. | msozeau | 2009-12-06 |
* | Fix anomaly when using typeclass resolution with filtered hyps in evars. | msozeau | 2009-12-06 |
* | Fix backtracking heuristic in typeclass resolution. | msozeau | 2009-11-30 |
* | Diamond-shape instead of linear hiearchy in Numbers/NatInt | letouzey | 2009-11-18 |
* | New syntax <+ for chains of Include (or Include Type) (or Include Self (Type)) | letouzey | 2009-11-16 |
* | Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxioms | letouzey | 2009-11-16 |
* | BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504) | letouzey | 2009-11-12 |
* | Repair interpretation of numeral for BigQ, add a printer (close #2160) | letouzey | 2009-11-12 |
* | SpecViaZ.NSig: all-in-one spec for [pred] and [sub] based on ZMax | letouzey | 2009-11-10 |
* | Simplification of Numbers, mainly thanks to Include | letouzey | 2009-11-10 |
* | Numbers: finish files NStrongRec and NDefOps | letouzey | 2009-11-06 |
* | Numbers: more (syntactic) changes toward new style of type classes | letouzey | 2009-11-06 |
* | Numbers: start using Classes stuff, Equivalence, Proper, Instance, etc | letouzey | 2009-11-03 |
* | Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False' | letouzey | 2009-10-08 |
* | Implicit argument of Logic.eq become maximally inserted | letouzey | 2009-10-08 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements | letouzey | 2009-09-09 |
* | Many fixes in unification: | msozeau | 2009-05-20 |
* | Rewrite autorewrite to use a dnet indexed by the left-hand sides (or | msozeau | 2009-04-14 |
* | Parsing files for numerals (+ ascii/string) moved into plugins | letouzey | 2009-03-27 |
* | Cyclic31: proof of a forgotten admit | letouzey | 2009-02-10 |
* | Uniformity with the rest of the StdLib : _symm --> _sym | letouzey | 2008-12-12 |
* | Add user syntax for creating hint databases [Create HintDb foo | msozeau | 2008-09-14 |
* | Even better test for choosing rewrite or setoid_rewrite. | msozeau | 2008-07-26 |
* | Autour du parsing: | herbelin | 2008-07-15 |
* | Fix bug #1899: no more strange notations for Qge and Qgt | letouzey | 2008-07-04 |
* | Various bug fixes in type classes and subtac: | msozeau | 2008-07-01 |
* | QMake : alternative equivalences with Qcanon thanks to earlier irreducibility... | letouzey | 2008-06-30 |
* | QMake: Proofs that add_norm and other ..._norm functions produce irreducible ... | letouzey | 2008-06-28 |
* | Enhanced discrimination nets implementation, which can now work with | msozeau | 2008-06-27 |
* | Some work on BigQ : | letouzey | 2008-06-25 |
* | Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk | herbelin | 2008-06-18 |
* | - Extension de "generalize" en "generalize c as id at occs". | herbelin | 2008-06-08 |
* | In abstract parts of theories/Numbers, plus/times becomes add/mul, | letouzey | 2008-06-03 |
* | In abstract parts of theories/Numbers, plus/times becomes add/mul, | letouzey | 2008-06-02 |
* | newton iteration for sqrt31 | thery | 2008-06-02 |
* | Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in | letouzey | 2008-06-01 |