index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
tacticals.mli
Commit message (
Expand
)
Author
Age
*
[api] Insert miscellaneous API deprecation back to core.
Emilio Jesus Gallego Arias
2017-11-13
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
[api] Deprecate all legacy uses of Name.Id in core.
Emilio Jesus Gallego Arias
2017-11-04
*
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
*
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
*
|
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
|
*
Fix the API of the new pf_constr_of_global.
Pierre-Marie Pédrot
2017-04-24
|
*
Removing the tclWEAK_PROGRESS tactical.
Pierre-Marie Pédrot
2017-04-24
|
*
Removing the tclNOTSAMEGOAL primitive from the API.
Pierre-Marie Pédrot
2017-04-24
|
/
*
Using delayed universe instances in EConstr.
Pierre-Marie Pédrot
2017-04-01
*
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
|
\
*
|
Removing most nf_enter in tactics.
Pierre-Marie Pédrot
2017-02-14
*
|
Do not ask for a normalized goal to get hypotheses and conclusions.
Pierre-Marie Pédrot
2017-02-14
*
|
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
*
|
Removing compatibility layers from Tacticals
Pierre-Marie Pédrot
2017-02-14
*
|
Cleaning up interfaces.
Pierre-Marie Pédrot
2017-02-14
*
|
Elim API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Tacticals API using EConstr.
Pierre-Marie Pédrot
2017-02-14
|
*
Proofview: tclINDEPENDENTL
Enrico Tassi
2017-02-10
|
/
*
Untangling Tacexpr from lower strata.
Pierre-Marie Pédrot
2016-09-15
*
Goal selectors are now tacticals and can be used as such.
Cyprien Mangin
2016-06-14
*
Tacticals: typo in a comment
Pierre Letouzey
2016-02-16
*
New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).
Hugo Herbelin
2016-01-21
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
*
|
Stronger invariants on the use of the introduction pattern (pat1,...,patn).
Hugo Herbelin
2016-01-21
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
merge
Matej Kosik
2016-01-11
|
\
\
|
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
|
Tentative API fix for tactic arguments to be fed to tclWITHHOLES.
Pierre-Marie Pédrot
2015-12-27
|
/
/
*
/
Indexing Proofview.goals with a stage.
Pierre-Marie Pédrot
2015-10-20
|
/
*
More expressive API for tclWITHHOLES.
Pierre-Marie Pédrot
2015-02-10
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
Update headers.
Maxime Dénès
2015-01-12
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Add Ltac syntax for the [tclIFCATCH] primitive.
Arnaud Spiwack
2014-12-12
*
Constructor tactics backtracking is done using [Tacticals.New] rather than [P...
Arnaud Spiwack
2014-12-08
*
Adding locations to tclZEROMSG.
Pierre-Marie Pédrot
2014-11-20
*
Lazy interpretation of patterns so that expressions such as "intros H H'/H"
Hugo Herbelin
2014-08-18
*
Adding a new intro-pattern for "apply in" on the fly. Using syntax
Hugo Herbelin
2014-08-18
*
Reorganisation of intropattern code
Hugo Herbelin
2014-08-18
*
Adding a "time" tactical for benchmarking purposes. In case the tactic
Hugo Herbelin
2014-07-13
*
Revert "time tac" (committed by mistake).
Hugo Herbelin
2014-07-07
*
time tac
Hugo Herbelin
2014-07-07
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
Using the new monad tactic in Inv.
Pierre-Marie Pédrot
2014-04-22
[next]