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
*
Implement the Export Set/Unset feature.
Pierre-Marie Pédrot
2018-03-09
*
Merge PR #6496: Generate typed generic code from ltac macros
Maxime Dénès
2018-03-09
|
\
*
\
Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...
Maxime Dénès
2018-03-08
|
\
\
*
\
\
Merge PR #6893: Cleanup UState API usage
Maxime Dénès
2018-03-08
|
\
\
\
|
|
|
*
Make most of TACTIC EXTEND macros runtime calls.
Maxime Dénès
2018-03-08
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #6918: romega: get rid of EConstr.Unsafe
Maxime Dénès
2018-03-08
|
\
\
\
*
\
\
\
Merge PR #6909: Deprecate Focus and Unfocus
Maxime Dénès
2018-03-08
|
\
\
\
\
*
\
\
\
\
Merge PR #6934: Warn when using “Require” in a section
Maxime Dénès
2018-03-08
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)
Maxime Dénès
2018-03-08
|
\
\
\
\
\
\
|
|
*
|
|
|
|
[stdlib] Do not use “Require” inside sections
Vincent Laporte
2018-03-07
|
|
/
/
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #6932: [stdlib] Do not use deprecated notations
Maxime Dénès
2018-03-07
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6905: Fix make ml-doc
Maxime Dénès
2018-03-07
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`
Maxime Dénès
2018-03-07
|
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
|
*
An experimental 'Show Extraction' command (grant feature wish #4129)
Pierre Letouzey
2018-03-06
|
|
|
|
|
|
|
|
*
Extraction: switch to EConstr.t as the central type to extract from.
Pierre Letouzey
2018-03-06
|
|
|
|
|
|
*
|
|
romega: get rid of EConstr.Unsafe
Pierre Letouzey
2018-03-06
|
|
|
|
|
|
|
|
/
|
|
|
|
|
|
|
/
|
|
|
|
*
|
|
/
|
[stdlib] Do not use deprecated notations
Vincent Laporte
2018-03-06
|
|
_
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
*
Rename some universe minimizing "normalize" functions to "minimize"
Gaëtan Gilbert
2018-03-06
|
|
|
|
|
|
*
Deprecate UState aliases in Evd.
Gaëtan Gilbert
2018-03-06
|
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.
Maxime Dénès
2018-03-06
|
\
\
\
\
\
\
|
|
|
|
*
|
|
ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)
Enrico Tassi
2018-03-06
*
|
|
|
|
|
|
Merge PR #6896: [compat] Remove NOOP deprecated options.
Maxime Dénès
2018-03-06
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"
Maxime Dénès
2018-03-06
|
\
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
Escape curly braces in ocamldoc comment
mrmr1993
2018-03-05
|
|
|
|
|
*
|
|
Separate vim/emacs fold markers from ocamldoc comments
mrmr1993
2018-03-05
|
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
[ssreflect] Export parsing witnesses in mli file.
Emilio Jesus Gallego Arias
2018-03-05
|
|
_
|
/
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-05
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monad
Maxime Dénès
2018-03-05
|
\
\
\
\
\
\
\
|
|
|
|
*
|
|
|
[compat] Remove NOOP and alias deprecated options.
Emilio Jesus Gallego Arias
2018-03-04
|
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
ssr: add Prenex Implicits for Some_inj to use it as a view
Anton Trunov
2018-03-04
|
|
|
|
*
|
|
ssr: fix typo in doc comment
Anton Trunov
2018-03-04
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
*
|
|
|
|
ssr: ipats: V82.tactic ~nf_evars:false everywhere
Enrico Tassi
2018-03-04
|
*
|
|
|
|
ssr: rewrite Ssripats and Ssrview in the tactic monad
Enrico Tassi
2018-03-04
*
|
|
|
|
|
Merge PR #6791: Removing compatibility support for versions older than 8.5.
Maxime Dénès
2018-03-04
|
\
\
\
\
\
\
|
|
/
/
/
/
/
|
/
|
|
|
|
|
*
|
|
|
|
|
Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.
Maxime Dénès
2018-03-04
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...
Maxime Dénès
2018-03-04
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6676: [proofview] goals come with a state
Maxime Dénès
2018-03-04
|
\
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
Remove all uses of Focus in standard library.
Théo Zimmermann
2018-03-04
|
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
*
[compat] Remove "Intuition Iff Unfolding"
Emilio Jesus Gallego Arias
2018-03-03
|
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
*
|
Turn warning for deprecated notations on.
Théo Zimmermann
2018-03-02
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
*
|
|
Moving code for "simple induction"/"simple destruct" to coretactics.ml4.
Hugo Herbelin
2018-03-01
|
|
/
/
/
|
/
|
|
|
|
|
*
|
[econstr] Continue consolidation of EConstr API under `interp`.
Emilio Jesus Gallego Arias
2018-02-28
|
|
/
/
|
/
|
|
*
|
|
Merge PR #6788: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in ...
Maxime Dénès
2018-02-28
|
\
\
\
|
|
|
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
|
|
_
|
/
|
/
|
|
*
|
|
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-22
*
|
|
Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`
Maxime Dénès
2018-02-21
|
\
\
\
*
\
\
\
Merge PR #6767: [ci] add elpi
Maxime Dénès
2018-02-21
|
\
\
\
\
|
|
|
|
*
proofview: goals come with a state
Enrico Tassi
2018-02-20
|
|
|
*
|
Fixes #6787 (minus sign interpreted by coqdoc as a bullet in Ring_theory.v).
Hugo Herbelin
2018-02-20
|
|
|
|
/
*
|
|
|
Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.
Hugo Herbelin
2018-02-20
[next]