index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
derive
Age
Commit message (
Expand
)
Author
2019-06-04
coqpp: add new ![] specifiers for structured proof interaction
Gaëtan Gilbert
2019-06-04
Proof_global: pass only 1 pstate when we don't want the proof stack
Gaëtan Gilbert
2019-05-14
Allow run_tactic to return a value, remove hack from ltac2
Gaëtan Gilbert
2019-03-27
[plugins] [derive] Adapt to removal of imperative proof state.
Emilio Jesus Gallego Arias
2019-03-14
Add relevance marks on binders.
Gaëtan Gilbert
2019-02-05
Make Program a regular attribute
Maxime Dénès
2019-01-24
[STM] explicit handling of parsing states
Enrico Tassi
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-11-17
[vernacextend] Consolidate extension points API
Emilio Jesus Gallego Arias
2018-10-02
Make the coqpp VERNAC EXTEND behave as the non-FUNCTIONAL camlp5 one.
Pierre-Marie Pédrot
2018-10-02
Port g_derive to coqpp.
Pierre-Marie Pédrot
2018-09-05
[build] Preliminary support for building Coq with `dune`.
Emilio Jesus Gallego Arias
2018-05-23
[api] Move `opacity_flag` to `Proof_global`.
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-17
Change references to CAMLP4 to CAMLP5 to be more accurate since we no
Jim Fehrle
2017-12-15
[econstr] Switch constrintern API to non-imperative style.
Emilio Jesus Gallego Arias
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-10-17
[stm] Remove state-handling from Futures.
Emilio Jesus Gallego Arias
2017-08-21
Ensuring all .v files end with a newline to make "sed -i" work better on them.
Hugo Herbelin
2017-07-17
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-10
Remove remaining vo.itarget files (obsolete since PR #499)
Pierre Letouzey
2017-06-07
Put all plugins behind an "API".
Matej Kosik
2017-05-27
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-02-14
Evar-normalizing functions now act on EConstrs.
Pierre-Marie Pédrot
2017-02-14
Removing various compatibility layers of tactics.
Pierre-Marie Pédrot
2016-09-22
Revert "Merge remote-tracking branch 'github/pr/283' into trunk"
Maxime Dénès
2016-09-22
Merge remote-tracking branch 'github/pr/283' into trunk
Maxime Dénès
2016-09-21
Merging Stdarg and Constrarg.
Pierre-Marie Pédrot
2016-09-20
Stylistic improvements in intf/decl_kinds.mli.
Maxime Dénès
2016-07-03
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-06-08
Compilation via pack for plugins of the stdlib
Pierre Letouzey
2016-05-08
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-03-17
Removing the special status of generic entries defined by Coq itself.
Pierre-Marie Pédrot
2016-02-09
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-10-29
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-28
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-09-08
Opacifying the proof_terminator type.
Pierre-Marie Pédrot
2015-03-11
admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)
Enrico Tassi
2015-02-14
Fixing OCaml 3.12 compilation.
Pierre-Marie Pédrot
2015-02-14
Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior
Enrico Tassi
2015-01-12
Update headers.
Maxime Dénès
2015-01-08
Avoiding introducing yet another convention in naming files.
Hugo Herbelin
