index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
funind
Commit message (
Expand
)
Author
Age
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-27
|
\
*
|
Adding ability to put any pattern in binders, prefixed by a quote.
Daniel de Rauglaudre
2016-06-27
*
|
Reuse the typing_flags datatype for inductives.
Pierre-Marie Pédrot
2016-06-18
*
|
Moving the typing_flags to the environment.
Pierre-Marie Pédrot
2016-06-18
*
|
Adding eintros to respect the e- prefix policy.
Hugo Herbelin
2016-06-18
*
|
Factorizing the uses of Declareops.safe_flags.
Pierre-Marie Pédrot
2016-06-16
*
|
Fixing a mispelling coma -> comma.
Hugo Herbelin
2016-06-16
*
|
Fixing printing of Function.
Hugo Herbelin
2016-06-16
*
|
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Pierre-Marie Pédrot
2016-06-16
|
\
\
|
*
|
Remove the syntax changes introduced by this branch.
Pierre-Marie Pédrot
2016-06-15
|
*
|
Assume totality: dedicated type rather than bool
Arnaud Spiwack
2016-06-14
*
|
|
Compilation via pack for plugins of the stdlib
Pierre Letouzey
2016-06-08
*
|
|
A slight phase of documentation and uniformization of names of
Hugo Herbelin
2016-06-02
*
|
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
|
*
Univs/Program/Function: Fix bug #4725
Matthieu Sozeau
2016-05-26
*
|
|
Put the "generalize" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
|
|
Put the "fix" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
|
|
Put the "clear" tactic into the monad.
Pierre-Marie Pédrot
2016-05-16
*
|
|
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
|
|
More toplevel value representation sharing.
Pierre-Marie Pédrot
2016-05-04
*
|
|
Revert "Fixing printing of Function."
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
*
|
|
Fixing printing of Function.
Hugo Herbelin
2016-04-27
*
|
|
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
*
|
|
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
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Rename Ephemeron -> CEphemeron.
Maxime Dénès
2016-03-04
*
|
|
Moving the Tauto tactic to proper Ltac.
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
|
*
|
|
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
*
|
|
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
*
|
|
|
Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.
Pierre-Marie Pédrot
2015-12-28
*
|
|
|
Tentative API fix for tactic arguments to be fed to tclWITHHOLES.
Pierre-Marie Pédrot
2015-12-27
|
/
/
/
*
|
|
CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified
Matej Kosik
2015-12-18
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-08
|
\
|
|
|
*
|
Fix some typos.
Guillaume Melquiond
2015-12-07
*
|
|
Removing redundant versions of generalize.
Hugo Herbelin
2015-12-05
*
|
|
Moving three related small half-general half-ad-hoc utility functions
Hugo Herbelin
2015-12-05
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-20
|
\
|
|
[next]