| Age | Commit message (Expand) | Author |
|---|
| 2009-11-21 | Lazier behaviour of [auto] when introducing hypothesis: query the hint db's o... | puech |
| 2009-11-19 | Refactoring of coqide backtrack code, with the intent to put everything | vgross |
| 2009-11-19 | Correction du bug #2118 (Coqdep does not escape #) | notin |
| 2009-11-18 | Now "Include Self <expr>" handles partially applied functors, cf for example ... | soubiran |
| 2009-11-18 | Diamond-shape instead of linear hiearchy in Numbers/NatInt | letouzey |
| 2009-11-18 | Allow interactive proofs in module types | letouzey |
| 2009-11-18 | Module subtyping : allow many <: and module type declaration with <: | letouzey |
| 2009-11-16 | 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 | Include Self (Type) Foo: applying a (Type) Functor to the current context | letouzey |
| 2009-11-16 | Some lemmas about dependent choice + extensions of Compare_dec + | herbelin |
| 2009-11-15 | Fix type class discharge again. | msozeau |
| 2009-11-15 | Document Generalizable Variables, and change syntax to | msozeau |
| 2009-11-15 | Fix [Instance: forall ..., C args := t] declarations to behave as | msozeau |
| 2009-11-13 | Move Obj.magic call to the Vm module | glondu |
| 2009-11-13 | Remove dubious call to Obj.magic (and dead code, by the way) | glondu |
| 2009-11-13 | Remove useless call to Obj.magic | glondu |
| 2009-11-13 | Make usages of the Obj module explicit | glondu |
| 2009-11-13 | Remove useless ppevd (which is identical to ppevm) | glondu |
| 2009-11-13 | scripting area now grabs focus at startup. | vgross |
| 2009-11-13 | new handling for lexical structures. | vgross |
| 2009-11-13 | lexing refactoring | vgross |
| 2009-11-13 | the inlining computation at functor application was raising not_found when th... | soubiran |
| 2009-11-13 | Fix test-suite scripts: [Generalizable Variables] and small | msozeau |
| 2009-11-12 | Backtrack on fixing #2167 | herbelin |
| 2009-11-12 | Suppression de l'appel à Lexing.new_line (qui n'existe pas dans les versions... | notin |
| 2009-11-12 | Oops, nf_evar_defs just changed to nf_evar_map. | msozeau |
| 2009-11-12 | Don't forget to normalize everything w.r.t. evars (fixes bug #2103). | msozeau |
| 2009-11-12 | Restore test-suite/csdp.cache erased from svn by mistake | letouzey |
| 2009-11-12 | BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504) | letouzey |
| 2009-11-12 | Experiment propagation of implicit arguments and arguments scope for | herbelin |
| 2009-11-12 | Addendum to revision 12501. | herbelin |
| 2009-11-12 | Repair interpretation of numeral for BigQ, add a printer (close #2160) | letouzey |
| 2009-11-11 | Better compatibility for Peqb | letouzey |
| 2009-11-11 | Promote evar_defs to evar_map (in Evd) | glondu |
| 2009-11-11 | Backtracking on the use of automatically generated schemes for | herbelin |
| 2009-11-11 | Added support for multiple where-clauses in Inductive and co (see wish #2163). | herbelin |
| 2009-11-11 | Redoing broken commit r12498 (fixing bug #2167 + attempt to test the | herbelin |
| 2009-11-11 | Fixing bug #2167 + attempt to test the compatibility of a more robust | herbelin |
| 2009-11-11 | Test for bug #2168, forgotten in r12496. | herbelin |
| 2009-11-11 | Fixed bug #2168 (closing a section may have as side-effect the erasure | herbelin |
| 2009-11-11 | Improving abbreviations/notations + backtrack of semantic change in r12439 | herbelin |
| 2009-11-10 | Compatibility ocaml <= 3.09 | herbelin |
| 2009-11-10 | Correction du bug #2183 | notin |
| 2009-11-10 | use only why-dp, support for z3 | marche |
| 2009-11-10 | 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 | DecidableType: A specification via boolean equality as an alternative to eq_dec | letouzey |
| 2009-11-09 | Deactivation of (intrusive) printing of abbreviations from non-imported modules. | herbelin |
| 2009-11-09 | Commit 12485 continued. | herbelin |
