| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 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 |
