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
*
Deprecate undocumented "intros until 0" in favor of "intros *".
Hugo Herbelin
2018-03-23
*
Merge PR #7028: Fix #7026: ssr: applying an overloaded lemma as a view takes ...
Enrico Tassi
2018-03-23
|
\
|
*
Fix #7026: ssr: applying an overloaded lemma as a view takes too long.
Pierre-Marie Pédrot
2018-03-21
*
|
[ssreflect] Respect Opaque in FO unification
Maxime Dénès
2018-03-20
|
/
*
[ssreflect] Fix module scoping problems due to packing and mli files.
Emilio Jesus Gallego Arias
2018-03-10
*
[located] Push inner locations in `reference` to a CAst.t node.
Emilio Jesus Gallego Arias
2018-03-09
*
[located] More work towards using CAst.t
Emilio Jesus Gallego Arias
2018-03-09
*
Merge PR #6775: Allow using cumulativity without forcing strict constraints.
Maxime Dénès
2018-03-09
|
\
*
\
Merge PR #6769: Split closure cache and remove whd_both
Maxime Dénès
2018-03-09
|
\
\
|
|
*
Allow using cumulativity without forcing strict constraints.
Gaëtan Gilbert
2018-03-09
*
|
|
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
|
\
\
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
Pass the constant cache as a separate argument in kernel reduction.
Pierre-Marie Pédrot
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
|
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
[next]