index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
tacticals.ml
Commit message (
Expand
)
Author
Age
*
Proofview: tclINDEPENDENTL
Enrico Tassi
2017-02-10
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-17
|
\
|
*
Fix bug #5139: Anomalies should not be caught by || / try.
Pierre-Marie Pédrot
2016-10-14
*
|
Untangling Tacexpr from lower strata.
Pierre-Marie Pédrot
2016-09-15
*
|
Unplugging Tacexpr in several interface files.
Pierre-Marie Pédrot
2016-09-08
*
|
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
\
*
|
|
CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...
Matej Kosik
2016-08-30
*
|
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
|
|
/
|
/
|
|
*
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
|
*
Remove errorlabstrm in favor of user_err
Emilio Jesus Gallego Arias
2016-08-19
|
*
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
|
/
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Optimize the subst tactic.
Pierre-Marie Pédrot
2016-06-24
*
Goal selectors are now tacticals and can be used as such.
Cyprien Mangin
2016-06-14
*
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
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
*
|
Fixing some problems with double induction.
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
|
/
/
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-20
|
\
|
|
*
More optimizations of [Clenv.clenv_fchain].
Pierre-Marie Pédrot
2015-11-17
*
|
Removing some goal unsafeness in inductive schemes.
Pierre-Marie Pédrot
2015-10-29
*
|
Proofview.Goal.sigma returns an indexed evarmap.
Pierre-Marie Pédrot
2015-10-20
*
|
Indexing Proofview.goals with a stage.
Pierre-Marie Pédrot
2015-10-20
*
|
Boxing the Goal.enter primitive into a record type.
Pierre-Marie Pédrot
2015-10-20
|
/
*
Univs: fix many evar_map initializations and leaks.
Matthieu Sozeau
2015-10-02
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Using tclZEROMSG instead of tclZERO in several places.
Pierre-Marie Pédrot
2015-04-23
*
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
*
Fixing #3896 (incorrect sigma given to printer).
Hugo Herbelin
2015-01-03
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Add Ltac syntax for the [tclIFCATCH] primitive.
Arnaud Spiwack
2014-12-12
*
Tentatively more informative report of failure when inferring
Hugo Herbelin
2014-12-11
*
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
*
Plural and singular forms in error messages.
Hugo Herbelin
2014-11-02
*
Proofview: split [V82] module into [Unsafe] and [V82].
Arnaud Spiwack
2014-10-22
*
Display number of available goals in "incorrect number of goals" error message.
Arnaud Spiwack
2014-09-08
*
Renaming goal-entering functions.
Pierre-Marie Pédrot
2014-09-06
*
Simplification of the tclCHECKINTERRUPT tactic.
Pierre-Marie Pédrot
2014-08-28
*
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
*
Improving error message when applying rewrite to an expression which is not a...
Hugo Herbelin
2014-08-18
[next]