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 #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
|
\
\
*
\
\
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: 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
*
|
|
|
Delete duplicate line
Paul Steckler
2018-01-30
|
/
/
/
|
*
/
Use r.(p) syntax to print primitive projections.
Maxime Dénès
2018-01-30
|
/
/
*
|
Remove dead code from funind.
Maxime Dénès
2018-01-24
*
|
Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.
Maxime Dénès
2018-01-18
|
\
\
|
*
|
Use let-in aware prod_applist_assum in dtauto and firstorder.
Jasper Hugunin
2018-01-17
*
|
|
Merge PR #6499: [vernac] Move the flags/attributes out of vernac_expr
Maxime Dénès
2018-01-16
|
\
\
\
*
\
\
\
Merge PR #6551: Bracket with goal selector
Maxime Dénès
2018-01-16
|
\
\
\
\
|
|
_
|
/
/
|
/
|
|
|
|
|
*
|
[vernac] vernac_expr no longer recursive
Vincent Laporte
2018-01-08
*
|
|
|
Merge PR #6497: Add optimize_heap tactic for #6488
Maxime Dénès
2018-01-08
|
\
\
\
\
|
|
_
|
/
/
|
/
|
|
|
|
|
|
*
Remove dir-locals and ship suggested helper hooks instead.
Gaëtan Gilbert
2018-01-06
|
|
_
|
/
|
/
|
|
[next]
Maxime Dénès
Emilio Jesus Gallego Arias
Enrico Tassi
Théo Zimmermann
Hugo Herbelin
Jim Fehrle
Joachim Breitner
Gaëtan Gilbert
Vincent Laporte
Paul Steckler
Jasper Hugunin