index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Deport the backtracking code out of the ide
vgross
2009-12-11
*
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
*
Migration of ProtectedToplevel and Line_oriented_parser into new contrib Inte...
letouzey
2009-12-08
*
Fix the build of coq via ocamlbuild
letouzey
2009-12-08
*
integrate MSetToFiniteSet into the compilation (and fix it)
letouzey
2009-12-08
*
Sos.ml: no more warnings
letouzey
2009-12-08
*
Declaremods.ml: a useless function wrongly introduced in last commit
letouzey
2009-12-08
*
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-07
*
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-06
*
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-03
*
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-02
*
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-12-01
*
Fix backtracking heuristic in typeclass resolution.
msozeau
2009-11-30
*
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-27
*
svn:ignore property
herbelin
2009-11-26
*
Fixing xml theory file export (was not consistent with coqdoc file
herbelin
2009-11-26
*
Fix for notation scope & inductive types
vsiles
2009-11-25
*
Minor fixes in typeclasses, avoiding repeated evar normalizations.
msozeau
2009-11-24
*
Small extra result on JMeq vs eq_dep.
herbelin
2009-11-24
*
Ergonomy and robustness fix
vgross
2009-11-23
*
Lazier behaviour of [auto] when introducing hypothesis: query the hint db's o...
puech
2009-11-21
*
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
[next]