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
*
Add an option to configure the modifier for Queries.
Cyprien Mangin
2016-06-02
*
Merge the user queries tab with the shortcut tab.
Cyprien Mangin
2016-06-02
*
Slightly better interface to edit queries.
Cyprien Mangin
2016-06-02
*
Add user-created queries to CoqIDE.
Cyprien Mangin
2016-06-02
*
Add a [Show Proof.] query to CoqIDE.
Cyprien Mangin
2016-06-02
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-01
|
\
*
|
Makefile.build : follow-up of previous commit
Pierre Letouzey
2016-06-01
*
|
Makefile.build : improved rules about .cm(x)a
Pierre Letouzey
2016-06-01
*
|
Makefile.build : update the otags rule
Pierre Letouzey
2016-06-01
*
|
g_tactics : remove opt_bindings (2-line dead code)
Pierre Letouzey
2016-06-01
*
|
Makefile.common : avoid warnings about files linked twice
Pierre Letouzey
2016-06-01
*
|
Merge branch 'yet-another-makefile-bigbang' into trunk
Pierre Letouzey
2016-06-01
|
\
\
|
*
|
Yet another Makefile reform : a unique phase without nasty make tricks
Pierre Letouzey
2016-06-01
|
*
|
Makefile: restore the use of coqdep_boot for creating .v.d files
Pierre Letouzey
2016-06-01
|
|
*
Fix potential race condition in vm_compute.
Guillaume Melquiond
2016-05-31
*
|
|
This patch splits pretty printing representation from IO operations.
Pierre-Marie Pédrot
2016-05-31
|
\
\
\
|
|
/
/
|
/
|
|
|
|
*
Revert "Rename Lexer -> CLexer."
Pierre-Marie Pédrot
2016-05-31
*
|
|
Making the grammar/ folder independent from the other ones.
Pierre-Marie Pédrot
2016-05-31
|
*
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
/
/
*
|
Checker: avoid using obsolete names from Names
Pierre Letouzey
2016-05-31
*
|
Checker: no more -I kernel via a few symlinks (for Names and Esubst)
Pierre Letouzey
2016-05-31
|
*
Extraction : add a location in the error message about polyprop
Pierre Letouzey
2016-05-30
*
|
Extraction : add a location in the error message about polyprop
Pierre Letouzey
2016-05-30
|
*
Fix bug #4746: Anomaly: Evar ?X10 was not declared.
Pierre-Marie Pédrot
2016-05-29
|
*
STM: fix argument filtering for slaves
Enrico Tassi
2016-05-27
|
*
Pfedit.get_current_context refinement (fix #4523)
Matthieu Sozeau
2016-05-26
|
*
rewrite/Univs: Fix bug # 4498.
Matthieu Sozeau
2016-05-26
*
|
Update required OCaml version in configure.
Maxime Dénès
2016-05-26
|
*
Extraction/Projections: Fix bug #4710
Matthieu Sozeau
2016-05-23
|
*
Hints/Univs: fix bug #4628 anomalies
Matthieu Sozeau
2016-05-23
*
|
typos
Enrico Tassi
2016-05-23
|
*
Disable memoization rather than failing when files cannot be opened.
Guillaume Melquiond
2016-05-20
*
|
Extraction: code cleanup in Common
Pierre Letouzey
2016-05-20
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-20
|
\
|
|
*
native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)
Pierre Letouzey
2016-05-19
|
*
Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)
Pierre Letouzey
2016-05-19
*
|
native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)
Pierre Letouzey
2016-05-19
*
|
Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)
Pierre Letouzey
2016-05-19
|
*
adding "user-contrib" directory to ".gitignore"
Matej Kosik
2016-05-19
|
*
Unicode.ascii_of_ident is now truly injective
Pierre Letouzey
2016-05-19
*
|
Unicode.ascii_of_ident is now truly injective
Pierre Letouzey
2016-05-19
*
|
Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/...
Pierre Letouzey
2016-05-19
*
|
Putting all the tactics exported by the Tactics module in the new monad API.
Pierre-Marie Pédrot
2016-05-17
|
\
\
|
*
|
Removing some compatibility layers in Tactics.
Pierre-Marie Pédrot
2016-05-17
|
*
|
Removing the old refine tactic from the Tactics module.
Pierre-Marie Pédrot
2016-05-17
|
*
|
Put the "move" tactic in the monad.
Pierre-Marie Pédrot
2016-05-17
|
*
|
Put the "change" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
|
*
|
Put the "specialize_eq" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
|
*
|
Put the "generalize dependent" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
|
*
|
Put the "generalize" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
[next]