index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
Commit message (
Expand
)
Author
Age
*
Revert "Fixing printers for pr_auto_using and pr_firstorder_using."
Hugo Herbelin
2016-04-27
*
Revert "Fixing printing of Function."
Hugo Herbelin
2016-04-27
*
Revert "Adding printers for ring and field commands."
Hugo Herbelin
2016-04-27
*
Revert "Fixing a mispelling coma -> comma."
Hugo Herbelin
2016-04-27
*
Fixing a mispelling coma -> comma.
Hugo Herbelin
2016-04-27
*
Adding printers for ring and field commands.
Hugo Herbelin
2016-04-27
*
Fixing printing of Function.
Hugo Herbelin
2016-04-27
*
Fixing printers for pr_auto_using and pr_firstorder_using.
Hugo Herbelin
2016-04-27
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-24
|
\
*
|
Bugfix micromega: more careful syntaxification of terms of the form (Rinv t)
Frédéric Besson
2016-04-18
*
|
Removing redundant *_TYPED AS clauses in EXTEND statements.
Pierre-Marie Pédrot
2016-04-12
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-09
|
\
\
|
|
*
Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v
Nickolai Zeldovich
2016-04-09
|
|
/
|
*
Fixing a source of inefficiency and an artificial dependency in the
Daniel de Rauglaudre
2016-04-08
*
|
Getting rid of the "_mods" parsing entry.
Pierre-Marie Pédrot
2016-04-01
*
|
Moving the proof mode parsing management to Pcoq.
Pierre-Marie Pédrot
2016-03-19
*
|
Removing the special status of generic arguments defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
*
|
Removing the special status of generic entries defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
*
|
Adding a universe argument to Pcoq.create_generic_entry.
Pierre-Marie Pédrot
2016-03-17
*
|
Removing the registering of default values for generic arguments.
Pierre-Marie Pédrot
2016-03-17
*
|
Supporting "(@foo) args" in patterns, where "@foo" has no arguments.
Hugo Herbelin
2016-03-13
*
|
Removing OCaml deprecated function names from the Lazy module.
Pierre-Marie Pédrot
2016-03-10
*
|
Removing useless grammar.cma dependencies.
Pierre-Marie Pédrot
2016-03-06
*
|
Splitting the nsatz ML module into an implementation and a grammar files.
Pierre-Marie Pédrot
2016-03-06
*
|
Moving Eauto to a simple ML file.
Pierre-Marie Pédrot
2016-03-06
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
|
*
|
Using build_selector from Equality as a replacement of the selector
Hugo Herbelin
2016-03-05
|
*
Rename Ephemeron -> CEphemeron.
Maxime Dénès
2016-03-04
*
|
Making parentheses mandatory in tactic scopes.
Pierre-Marie Pédrot
2016-03-04
*
|
Getting rid of the "<:tactic< ... >>" quotations.
Pierre-Marie Pédrot
2016-02-24
*
|
Moving the Tauto tactic to proper Ltac.
Pierre-Marie Pédrot
2016-02-22
*
|
The tactic generic argument now returns a value rather than a glob_expr.
Pierre-Marie Pédrot
2016-02-22
*
|
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
\
*
|
|
Using monotonic types for conversion functions.
Pierre-Marie Pédrot
2016-02-15
*
|
|
More conversion functions in the new tactic API.
Pierre-Marie Pédrot
2016-02-15
*
|
|
Moving conversion functions to the new tactic API.
Pierre-Marie Pédrot
2016-02-15
*
|
|
Renaming functions in Typing to stick to the standard e_* scheme.
Pierre-Marie Pédrot
2016-02-15
*
|
|
Monotonizing the Evarutil module.
Pierre-Marie Pédrot
2016-02-15
|
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
|
/
/
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
|
*
Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.
Maxime Dénès
2016-01-15
*
|
CLEANUP: removing unused field
Matej Kosik
2016-01-11
*
|
merge
Matej Kosik
2016-01-11
|
\
\
|
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
|
Merge remote-tracking branch 'origin/v8.5' into trunk
Guillaume Melquiond
2016-01-06
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Protect code against changes in Map interface.
Maxime Dénès
2016-01-06
*
|
|
Merge remote-tracking branch 'origin/v8.5' into trunk
Guillaume Melquiond
2016-01-05
|
\
|
|
|
*
|
Extraction: msg_notice instead of msg_info.
Pierre Courtieu
2016-01-04
*
|
|
Fix typos.
Guillaume Melquiond
2016-01-01
[next]
Hugo Herbelin
Pierre-Marie Pédrot
Frédéric Besson
Nickolai Zeldovich
Daniel de Rauglaudre
Maxime Dénès
Matej Kosik
Guillaume Melquiond
Pierre Courtieu