index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
Commit message (
Expand
)
Author
Age
*
Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).
Maxime Dénès
2017-10-04
|
\
*
|
Efficient computation of the names contained in an environment.
Pierre-Marie Pédrot
2017-09-28
*
|
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-09-28
*
|
Merge PR #688: Binding universe constraints in Definition/Inductive/etc...
Maxime Dénès
2017-09-26
|
\
\
*
\
\
Merge PR #1060: An optimization of tactic constructor
Maxime Dénès
2017-09-25
|
\
\
\
*
|
|
|
Mark "Set Tactic Compat Context" as deprecated.
Guillaume Melquiond
2017-09-21
|
*
|
|
An optimization of tactic constructor.
Hugo Herbelin
2017-09-19
|
/
/
/
|
|
*
Fixing bug #5741 (anomaly in info_trivial).
Hugo Herbelin
2017-09-19
|
|
/
|
/
|
*
|
Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).
Maxime Dénès
2017-09-19
|
\
\
|
|
*
Don't lose names in UState.universe_context.
Gaëtan Gilbert
2017-09-19
|
|
/
|
/
|
*
|
Merge PR #1046: Better error messages, fix for BZ#5723
Maxime Dénès
2017-09-15
|
\
\
*
\
\
Merge PR #1037: Parse directly to Sorts.family when appropriate.
Maxime Dénès
2017-09-15
|
\
\
\
*
\
\
\
Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In...
Maxime Dénès
2017-09-15
|
\
\
\
\
|
|
|
|
*
Avoid extra failure in the "constructor" tactic (bug #5666).
Guillaume Melquiond
2017-09-14
|
|
_
|
_
|
/
|
/
|
|
|
|
|
|
*
Better error messages, fix for BZ#5723
Paul Steckler
2017-09-11
|
|
_
|
/
|
/
|
|
|
|
*
Parse directly to Sorts.family when appropriate.
Gaëtan Gilbert
2017-09-08
|
|
/
|
/
|
*
|
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-09-04
|
*
Fixing part of #5707 (allowing destruct to use non dependent case analysis).
Hugo Herbelin
2017-08-30
*
|
Fix BZ#5697: Congruence does not work with primitive projections.
Pierre-Marie Pédrot
2017-08-29
*
|
Merge PR #830: Moving assert (the "Cut" rule) to new proof engine
Maxime Dénès
2017-08-29
|
\
\
*
\
\
Merge PR #805: Functional tactics
Maxime Dénès
2017-08-29
|
\
\
\
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).
Maxime Dénès
2017-08-01
|
\
\
\
*
\
\
\
Merge PR #919: Remove a few useless evar-normalizations in printing code.
Maxime Dénès
2017-08-01
|
\
\
\
\
*
\
\
\
\
Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead
Maxime Dénès
2017-07-31
|
\
\
\
\
\
|
|
|
|
*
|
better `try with` scope in `discr_positions`
amblaf
2017-07-31
|
|
|
|
*
|
Correcting [build_discriminator] to make the test-suite pass
amblaf
2017-07-31
|
|
|
|
*
|
Replacing tclENV with the goal environment
amblaf
2017-07-31
|
|
|
|
*
|
env, sigma as first arguments of functions
amblaf
2017-07-31
|
|
|
|
*
|
Remove references to Global.env in tactics/*.ml
amblaf
2017-07-31
|
|
_
|
_
|
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #888: Stronger kernel types
Maxime Dénès
2017-07-28
|
\
\
\
\
\
|
|
|
|
*
|
Fixing bug #5671 (specialize unclean wrt Metas).
Hugo Herbelin
2017-07-27
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
*
|
|
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
|
|
|
*
|
Remove a few useless evar-normalizations in printing code.
Pierre-Marie Pédrot
2017-07-26
|
|
_
|
/
/
|
/
|
|
|
|
*
|
|
More precise type for universe entries.
Pierre-Marie Pédrot
2017-07-26
|
|
/
/
*
|
|
Merge PR #868: Fix debug trace of typeclasses eauto.
Maxime Dénès
2017-07-26
|
\
\
\
|
|
/
/
|
/
|
|
*
|
|
Merge PR #892: Improve do_split option of typeclass resolution
Maxime Dénès
2017-07-20
|
\
\
\
*
\
\
\
Merge PR #899: [general] Move files to directories so they match linking order.
Maxime Dénès
2017-07-20
|
\
\
\
\
*
\
\
\
\
Merge PR #869: Enforce alternating separators in typeclass debug output
Maxime Dénès
2017-07-20
|
\
\
\
\
\
*
\
\
\
\
\
Merge branch 'v8.7'
Maxime Dénès
2017-07-20
|
\
\
\
\
\
\
|
|
|
*
|
|
|
[general] Move files to directories matching linking order.
Emilio Jesus Gallego Arias
2017-07-19
|
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
Fix debug trace of typeclasses eauto.
Théo Zimmermann
2017-07-19
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
*
|
Improve do_split option of typeclass resolution
Matthieu Sozeau
2017-07-18
|
|
_
|
/
/
|
/
|
|
|
*
|
|
|
Getting rid of abstraction breaking code in tclABSTRACT.
Pierre-Marie Pédrot
2017-07-14
*
|
|
|
Remove the function Global.type_of_global_unsafe.
Pierre-Marie Pédrot
2017-07-13
*
|
|
|
Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.
Pierre-Marie Pédrot
2017-07-13
*
|
|
|
Getting rid of AUContext abstraction breakers in Elimschemes.
Pierre-Marie Pédrot
2017-07-13
|
|
*
|
format pairs of items for pr_depth to get alternating separators
Paul Steckler
2017-07-12
|
*
|
|
Backtracking on deprecation of Bracketing Last Intro Pattern.
Théo Zimmermann
2017-07-11
|
*
|
|
Deprecate options that were introduced for compatibility with 8.5.
Théo Zimmermann
2017-07-11
|
|
/
/
*
/
/
Safe API for accessing universe constraints of global references.
Pierre-Marie Pédrot
2017-07-11
|
/
/
[next]
Maxime Dénès
Pierre-Marie Pédrot
Guillaume Melquiond
Hugo Herbelin
Gaëtan Gilbert
Paul Steckler
amblaf
Matej Košík
Emilio Jesus Gallego Arias
Théo Zimmermann
Matthieu Sozeau