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 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
|
\
\
\
|
|
|
*
[stdlib] Do not use deprecated notations
Vincent Laporte
2018-03-06
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.
Maxime Dénès
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
|
\
\
\
\
\
\
|
|
|
|
|
|
*
[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
*
|
|
|
Adding support for parsing subterms of a notation as "pattern".
Hugo Herbelin
2018-02-20
*
|
|
|
Adding patterns in the category of binders for notations.
Hugo Herbelin
2018-02-20
*
|
|
|
Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.
Hugo Herbelin
2018-02-20
|
|
_
|
/
|
/
|
|
|
*
|
pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)
Enrico Tassi
2018-02-19
|
/
/
*
|
Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`
Maxime Dénès
2018-02-19
|
\
\
*
\
\
Merge PR #6648: [tactics] make apply_type safe
Maxime Dénès
2018-02-19
|
\
\
\
*
\
\
\
Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...
Maxime Dénès
2018-02-19
|
\
\
\
\
*
\
\
\
\
Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.
Maxime Dénès
2018-02-19
|
\
\
\
\
\
|
|
*
|
|
|
Change references to CAMLP4 to CAMLP5 to be more accurate since we no
Jim Fehrle
2018-02-17
|
|
|
*
|
|
apply_type: add option "typecheck" passed down to refine
Enrico Tassi
2018-02-16
|
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
*
Extend `zify_N` with knowledge about `N.pred`
Joachim Breitner
2018-02-14
|
|
_
|
_
|
/
|
/
|
|
|
|
|
|
*
[engine] Remove ghost parameter from `Proofview.Goal.t`
Emilio Jesus Gallego Arias
2018-02-12
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #6651: Use r.(p) syntax to print primitive projections.
Maxime Dénès
2018-02-12
|
\
\
\
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding
Maxime Dénès
2018-02-07
|
\
\
\
*
\
\
\
Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in Ve...
Maxime Dénès
2018-02-05
|
\
\
\
\
|
|
*
|
|
Reductionops.nf_* now take an environment.
Gaëtan Gilbert
2018-02-02
|
|
/
/
/
|
/
|
|
|
|
*
|
|
[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition
Vincent Laporte
2018-02-01
[next]