index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2016-08-18
Merge remote-tracking branch 'github/bug4978' into v8.6
Matthieu Sozeau
2016-08-18
Merge remote-tracking branch 'github/bug4188' into v8.6
Matthieu Sozeau
2016-08-18
Fix an occurrence of deprecated eqn syntax in stdlib.
Maxime Dénès
2016-08-18
Fix bug #4939: LtacProf prints tactic notations weirdly.
Pierre-Marie Pédrot
2016-08-18
Adding a test for bug #4653.
Pierre-Marie Pédrot
2016-08-18
Merge PR #256 into v8.6
Pierre-Marie Pédrot
2016-08-17
In docs, fix command to reset Ltac profiling
Paul Steckler
2016-08-17
Fix setoid_rewrite to raise proper errors
Matthieu Sozeau
2016-08-17
Documenting fix of #3070 (subst and chain of dependencies).
Hugo Herbelin
2016-08-17
Fix #4978: priorities of Equivalence instances
Matthieu Sozeau
2016-08-17
Fixing #3070 ("subst" taking properly into account chains of dependencies).
Hugo Herbelin
2016-08-17
Two protections against failures when printing evar_map.
Hugo Herbelin
2016-08-17
Fixing printing in debugger (no global env in debugger).
Hugo Herbelin
2016-08-17
A fix to dev/include.
Hugo Herbelin
2016-08-16
Removing dead unsafe debugging code in Constrintern.
Pierre-Marie Pédrot
2016-08-16
Merge PR #250 into v8.6
Pierre-Marie Pédrot
2016-08-16
Merge PR #237 into v8.6
Pierre-Marie Pédrot
2016-08-16
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-08-16
Efficiently generate the pretyping contexts.
Pierre-Marie Pédrot
2016-08-16
Merge branch 'pr255' into v8.5 (bug #5015)
Guillaume Melquiond
2016-08-14
Fix regression in Coqide's "forward one command" command
Xavier Leroy
2016-08-11
Do not assume the "TERM" environment variable is always set (bug #5007).
Guillaume Melquiond
2016-08-11
Use the "md5" command on OpenBSD (bug #5008).
Guillaume Melquiond
2016-08-10
Make code a bit clearer by removing optional argument.
Guillaume Melquiond
2016-08-10
Remove unused optional "predicative" argument.
Guillaume Melquiond
2016-08-10
Make it a bit more obvious when variables are of type unit.
Guillaume Melquiond
2016-08-09
Reduce warning noise when compiling the standard library.
Guillaume Melquiond
2016-08-09
Make List.map_filter(_i) tail-recursive.
Guillaume Melquiond
2016-08-07
Fix #5000: Document the native compiler soundness bug due to Unicode mangling.
Pierre-Marie Pédrot
2016-08-06
Using a dedicated kind of substitutions in evar name generation.
Pierre-Marie Pédrot
2016-08-05
Using the extended contexts in pretyping.
Pierre-Marie Pédrot
2016-08-04
Use sets instead of lists for names to avoid in evar generation.
Pierre-Marie Pédrot
2016-08-04
Simplifying code in evar generation.
Pierre-Marie Pédrot
2016-08-04
Exporting the renaming API for evar declaration.
Pierre-Marie Pédrot
2016-08-04
Embedding the pretyping environment in a dummy record.
Pierre-Marie Pédrot
2016-08-04
Fix documentation typo (bug #4994).
Guillaume Melquiond
2016-07-29
Fix bug #4673: regression in setoid_rewrite.
Matthieu Sozeau
2016-07-29
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Matthieu Sozeau
2016-07-29
Update CHANGES about #3886 bugfix
Matthieu Sozeau
2016-07-29
Fix bug #3886, generation of obligations of fixes
Matthieu Sozeau
2016-07-29
Fix #4769, univ poly and elim schemes in sections
Matthieu Sozeau
2016-07-29
COMMENT: moving misplaced comment where it belongs
Matej Kosik
2016-07-26
Adding a flag in CoqIDE to configure UNIX/Windows line ending.
Pierre-Marie Pédrot
2016-07-26
restore compatibility with gallium's camlp4 (broken by commit 8e07227c)
Pierre Letouzey
2016-07-26
Update CHANGES about critical bugfix and others
Matthieu Sozeau
2016-07-26
Merge branch 'bug4754' into v8.5
Matthieu Sozeau
2016-07-26
Fix bug #4754, allow conversion problems to remain
Matthieu Sozeau
2016-07-26
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Matthieu Sozeau
2016-07-26
Merge branch 'bug4876' into v8.5
Matthieu Sozeau
2016-07-25
Merge remote-tracking branch 'github/bug4679' into v8.6
Matthieu Sozeau
[next]