| Age | Commit message (Expand) | Author |
|---|
| 2009-12-08 | Declaremods.ml: a useless function wrongly introduced in last commit | letouzey |
| 2009-12-07 | Fix bug #2197 (option show_toolbar not taken into account at startup) | vgross |
| 2009-12-07 | Remove the "detach script windows" feature. | vgross |
| 2009-12-07 | No more specific syntax "Include Self" for inclusion of partially-applied fun... | letouzey |
| 2009-12-07 | revert on commit r12553 | barras |
| 2009-12-06 | Turn evars created by a tactic application into a subgoal immediately in | msozeau |
| 2009-12-06 | Forgot a file in last commit. | msozeau |
| 2009-12-06 | Fix anomaly when using typeclass resolution with filtered hyps in evars. | msozeau |
| 2009-12-03 | Still continuing r12485-12486, r12549, r12556 (cleaning around name generation) | herbelin |
| 2009-12-03 | Restored rewriting of JMeq using JMeq_rect and co when the domains are the same | herbelin |
| 2009-12-03 | Fix bug #2191 : Serious "undo" performance degradation since 8.2pl1 | vgross |
| 2009-12-03 | declaremods.ml <--- code factoring | soubiran |
| 2009-12-03 | Rename proper to proper_prf to avoid clash with CoRN, | msozeau |
| 2009-12-02 | Continuing r12485-12486 and r12549 (cleaning around name generation) | herbelin |
| 2009-12-02 | Remove interface plugin | glondu |
| 2009-12-02 | Update .gitignore | glondu |
| 2009-12-01 | two improvements of the guard condition: | barras |
| 2009-12-01 | fix coqchk options documentation | barras |
| 2009-12-01 | install manpage of coqchk | barras |
| 2009-12-01 | Fix make_exact_entry to allow applying [forall x, P x] hints directly, | msozeau |
| 2009-12-01 | Continuing r12485-12486 (cleaning around name generation) | herbelin |
| 2009-12-01 | Fix bug in typeclass resolution. Better handling of universes in | msozeau |
| 2009-11-30 | Fix backtracking heuristic in typeclass resolution. | msozeau |
| 2009-11-27 | Added support for definition of fixpoints using tactics. | herbelin |
| 2009-11-27 | Substitute terms for evars-as-goals as soon as they are solved in | msozeau |
| 2009-11-26 | svn:ignore property | herbelin |
| 2009-11-26 | Fixing xml theory file export (was not consistent with coqdoc file | herbelin |
| 2009-11-25 | Fix for notation scope & inductive types | vsiles |
| 2009-11-24 | Minor fixes in typeclasses, avoiding repeated evar normalizations. | msozeau |
| 2009-11-24 | Small extra result on JMeq vs eq_dep. | herbelin |
| 2009-11-23 | Ergonomy and robustness fix | vgross |
| 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 |
