index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
derive
/
derive.ml
Age
Commit message (
Expand
)
Author
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-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-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-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-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
