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
*
An generic imperative union-find, used for deps of evars in Class_tactics
letouzey
2011-02-11
*
Change Evd.fold to a faster version that simply removes unneeded evars.
msozeau
2011-02-11
*
compatibility <3.12 (Map.exists Map.singleton)
pboutill
2011-02-11
*
Remove obsolete TheoryList
glondu
2011-02-10
*
Vectors fully use implicit arguments
pboutill
2011-02-10
*
Fixpoints are traverse during implicits arguments search to toplevel
pboutill
2011-02-10
*
Interp a definition with the implicit arguments of its local context
pboutill
2011-02-10
*
local variables can have implicits locally
pboutill
2011-02-10
*
Data structure telling implicits of local variables is a map in the
pboutill
2011-02-10
*
internalize now use a record for its env
pboutill
2011-02-10
*
MacOS compatibility
pboutill
2011-02-10
*
More comments and less doublons in some mli
pboutill
2011-02-10
*
- proper printing of setoid_rewrite tactic applications
msozeau
2011-02-10
*
Rename subst_raw_with_bindings to subst_glob_with_bindings and export
msozeau
2011-02-10
*
Started to fix the declarative proof mode (C-zar).
aspiwack
2011-02-10
*
One more fix for setoid_rewrite: completely reinterpret the given lemmas
msozeau
2011-02-09
*
Correct handling of existential variables when multiple different
msozeau
2011-02-08
*
Factorize code of rewrite to make way for a new implementation using the
msozeau
2011-02-07
*
Dp: another fix suggested by Virgile Prevosto
letouzey
2011-02-03
*
Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)
letouzey
2011-02-03
*
Coqlib.gen_constant_in_modules can take a qualid string "Foo.bar"
letouzey
2011-01-31
*
A fine-grain control of inlining at functor application via priority levels
letouzey
2011-01-31
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
test-suite/Makefile: add a rule to build all_stdlib.v (for the bench)
glondu
2011-01-27
*
Make simpl use the proper constant when folding (mutual) fixpoints
letouzey
2011-01-27
*
Fix compilation with camlp5 (Closes: #2487)
glondu
2011-01-25
*
Update .gitignore
glondu
2011-01-25
*
Add a test for sorting all universes of stdlib
glondu
2011-01-25
*
Rewrite sort_universes to minimize the number of universes
glondu
2011-01-25
*
Numbers: simplier spec for testbit
letouzey
2011-01-20
*
Fix formatting issue in refman
glondu
2011-01-12
*
Fix ocamlbuild-based build system
glondu
2011-01-11
*
Remove references to -ide option of coqmktop
glondu
2011-01-11
*
In univ.ml, put universe_level primitives in its their own sub-module
glondu
2011-01-11
*
Add [Typeclasses Debug] option that respects backtracking, solve
msozeau
2011-01-11
*
Add "Print Sorted Universes"
glondu
2011-01-11
*
Use dashed lines for equivalence edges in dot output of universes
glondu
2011-01-11
*
More coherent comment ordering
glondu
2011-01-11
*
Fix some typos
glondu
2011-01-11
*
ratrapage exception, deja fait ...
bgregoir
2011-01-11
*
Fixing an uncaught exception bug with use of vmcast
herbelin
2011-01-07
*
MacOS integration
pboutill
2011-01-07
*
Separate load_file handler in coqide
pboutill
2011-01-07
*
Coqide is not built with coqmktop any more
pboutill
2011-01-07
*
Don't install both coqide.byte and coqide.opt
pboutill
2011-01-07
*
Call coqtop with -nois when probing for files
pboutill
2011-01-07
*
Fix print in coqide
pboutill
2011-01-07
*
mli comments for doc
pboutill
2011-01-07
*
Update CHANGES
pboutill
2011-01-07
*
Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)
letouzey
2011-01-07
[next]