aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.ml
Commit message (Expand)AuthorAge
* Proofview: tclINDEPENDENTLGravatar Enrico Tassi2017-02-10
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\
| * Fix bug #5139: Anomalies should not be caught by || / try.Gravatar Pierre-Marie Pédrot2016-10-14
* | Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
* | Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* | | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| |/ |/|
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Optimize the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* Goal selectors are now tacticals and can be used as such.Gravatar Cyprien Mangin2016-06-14
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).Gravatar Hugo Herbelin2016-01-21
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
* | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
* | Fixing some problems with double induction.Gravatar Hugo Herbelin2016-01-21
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-12-27
|/ /
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-20
|\|
| * More optimizations of [Clenv.clenv_fchain].Gravatar Pierre-Marie Pédrot2015-11-17
* | Removing some goal unsafeness in inductive schemes.Gravatar Pierre-Marie Pédrot2015-10-29
* | Proofview.Goal.sigma returns an indexed evarmap.Gravatar Pierre-Marie Pédrot2015-10-20
* | Indexing Proofview.goals with a stage.Gravatar Pierre-Marie Pédrot2015-10-20
* | Boxing the Goal.enter primitive into a record type.Gravatar Pierre-Marie Pédrot2015-10-20
|/
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Using tclZEROMSG instead of tclZERO in several places.Gravatar Pierre-Marie Pédrot2015-04-23
* More expressive API for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-02-10
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing #3896 (incorrect sigma given to printer).Gravatar Hugo Herbelin2015-01-03
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Constructor tactics backtracking is done using [Tacticals.New] rather than [P...Gravatar Arnaud Spiwack2014-12-08
* Adding locations to tclZEROMSG.Gravatar Pierre-Marie Pédrot2014-11-20
* Plural and singular forms in error messages.Gravatar Hugo Herbelin2014-11-02
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Display number of available goals in "incorrect number of goals" error message.Gravatar Arnaud Spiwack2014-09-08
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Simplification of the tclCHECKINTERRUPT tactic.Gravatar Pierre-Marie Pédrot2014-08-28
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Improving error message when applying rewrite to an expression which is not a...Gravatar Hugo Herbelin2014-08-18