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
...
*
Added Add LoadPath in coqdep lexer (but not in coqdep itself by lack of time).
herbelin
2011-10-29
*
Fixed broken globalization of identifiers containing utf8 letters
herbelin
2011-10-29
*
Added checksums to glob files and warned about possibly missing
herbelin
2011-10-29
*
Remove dynamic stuff from constr_expr and glob_constr
glondu
2011-10-28
*
Remove avoidable use of GDynamic
glondu
2011-10-27
*
Deactivating second-order pattern-matching in evarconv for 8.4.
herbelin
2011-10-26
*
Fix configuration box bug in recursive call
pboutill
2011-10-26
*
Coq_makefile handles .mlpack files
pboutill
2011-10-26
*
Coqdep handles .mlpack
pboutill
2011-10-26
*
Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)
letouzey
2011-10-26
*
When checking for emptiness, use Foo.is_empty instead of (=) Foo.empty
letouzey
2011-10-26
*
Environ.set_universes is dead code
letouzey
2011-10-26
*
Mod_subst: some simplifications, some more significant names to functions, etc
letouzey
2011-10-26
*
Auto: avoid storing clausenv (and hence env, evar_map, universes) in vo
letouzey
2011-10-26
*
Makefile install rule fix
pboutill
2011-10-26
*
Coq_makefile includes coqtop -config without file generation
pboutill
2011-10-26
*
Coq_makefile: libraries in bytecode are now installed too
pboutill
2011-10-26
*
Revision 14605 continued (Utf8.v now correctly exporting Utf8_core.v).
herbelin
2011-10-26
*
Applying Tom Prince's patch to support parametric "constructor n" in
herbelin
2011-10-25
*
Merge common notations from Utf8.v and Utf8_core.v (see bug report #2610).
herbelin
2011-10-25
*
Regression tests for bugs #2613 and #2616.
herbelin
2011-10-25
*
First attempt at making Print Assumption compatible with opaque modules (fix ...
letouzey
2011-10-25
*
Coq_makefile: a more complete commentary about global variables
pboutill
2011-10-25
*
Coq_makefile does not install/compile explicitely cmo and cmxs? that are in a...
pboutill
2011-10-25
*
coqdep defines a makefile variable name_MLLIB_DEPENDENCIES to store dependenc...
pboutill
2011-10-25
*
Fixing use of type constraint for refining the "return" clause of "match".
herbelin
2011-10-25
*
Continuing r14585 (ill-typed restriction bug).
herbelin
2011-10-25
*
Fixing "destruct" test.
herbelin
2011-10-25
*
Continuing r1492 (useless changes were inadvertantly committed)
herbelin
2011-10-25
*
New strategy to infer return predicate of match construct when
herbelin
2011-10-25
*
Still more unification in typing.ml
herbelin
2011-10-25
*
Icons in CoqIdE preference panel
pboutill
2011-10-25
*
Configuration window of CoqIdE looks more like other Gtk one.
pboutill
2011-10-25
*
Heads: avoid potentially uncaught Not_found via an assert false
letouzey
2011-10-24
*
Mod_subst: Attempt to fix #2608
letouzey
2011-10-24
*
More unification in type_of and addition of e_type_of to get the new
herbelin
2011-10-24
*
Fixing another bug revealing ill-typed use of evar restriction.
herbelin
2011-10-24
*
Fixing instance/filter mismatch in materialize_evar + documentation.
herbelin
2011-10-24
*
Fixing failing printer when the type of a binder name with implicit
herbelin
2011-10-24
*
Fail if some conv pbs remain after consider_remaining_unif_problems.
herbelin
2011-10-22
*
Now consider remaining conversion problems in solve_remaining_evars.
herbelin
2011-10-22
*
Use also second-order unification if first-order fails at the time of conside...
herbelin
2011-10-22
*
Use full conversion for checking type of holes in destruct over a
herbelin
2011-10-22
*
Fixing uncaught exception in pr_evar_map (pr_global failed for unknown global...
herbelin
2011-10-22
*
Fixing Equality.injectable which did not detect an equality without
herbelin
2011-10-22
*
More descriptive error messages in checker
glondu
2011-10-20
*
Extraction.tex: typo in an Extract Inductive example (fix #2625)
letouzey
2011-10-18
*
Fix bug #2473 due to wrong folding of the evar environment
msozeau
2011-10-18
*
Fix bug #2227
msozeau
2011-10-18
*
Fix inductive coercion code in Program (bug #2378)
msozeau
2011-10-18
[prev]
[next]