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
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-04
|
\
|
*
Fix Haskell extraction for terms over 45 characters long
Nickolai Zeldovich
2016-05-04
|
*
Handle primitive projections inside types when extracting (bug #4616).
Guillaume Melquiond
2016-05-04
*
|
Merge branch 'haskell-type-indent' of https://github.com/zeldovich/coq into t...
Pierre Letouzey
2016-05-04
|
\
\
|
|
*
Remove extraneous space in coqtop/pg output (bug #4675).
Guillaume Melquiond
2016-05-03
*
|
|
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
|
|
*
Fix Haskell extraction for terms over 45 characters long
Nickolai Zeldovich
2016-02-19
|
|
/
|
/
|
*
|
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
|
\
\
[next]