| Commit message (Expand) | Author | Age |
* | 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-19 |
* | 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-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 |
* | 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-16 |
* | 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-15 |
* | 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-13 |
* | 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-12 |
* | 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-11 |
* | 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-10 |
* | Deactivation of (intrusive) printing of abbreviations from non-imported modules. | herbelin | 2009-11-09 |
* | Commit 12485 continued. | herbelin | 2009-11-09 |
* | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin | 2009-11-09 |