aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/extratactics.ml4
Commit message (Expand)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* FIx parsing of tactic "simple refine".Gravatar Maxime Dénès2015-12-16
* Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".Gravatar Guillaume Melquiond2015-12-16
* Refine tactic now shelves unifiable holes.Gravatar Pierre-Marie Pédrot2015-12-15
* Changing the order of the goals generated by unshelve.Gravatar Pierre-Marie Pédrot2015-12-15
* Fixing parsing of the unshelve tactical.Gravatar Pierre-Marie Pédrot2015-12-09
* Adding an unshelve tactical.Gravatar Pierre-Marie Pédrot2015-12-09
* Fix [Polymorphic Hint Rewrite].Gravatar Matthieu Sozeau2015-11-27
* Univs: refined handling of assumptionsGravatar Matthieu Sozeau2015-10-02
* Univs: fix evar_map handling in Hint processing.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* Hopefully better names to constructors of internal_flag, as discussedGravatar Hugo Herbelin2015-09-23
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Using tclZEROMSG instead of tclZERO in several places.Gravatar Pierre-Marie Pédrot2015-04-23
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* More expressive API for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-02-10
* Revert "Removing spurious tclWITHHOLES."Gravatar Pierre-Marie Pédrot2015-02-10
* Update headers.Gravatar Maxime Dénès2015-01-12
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Gravatar Hugo Herbelin2014-12-07
* Used an evar name based on the local def name in "evar" tactic.Gravatar Hugo Herbelin2014-11-25
* new: Optimize Proof, Optimize HeapGravatar Enrico Tassi2014-11-09
* Removing the legacy intro tactic code.Gravatar Pierre-Marie Pédrot2014-11-07
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Remove the deprecated open-constr based refine.Gravatar Arnaud Spiwack2014-10-22
* Proofview.Refine: remove the handle type, and simplify the API.Gravatar Arnaud Spiwack2014-10-16
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* Rename eq_constr functions in Evd to not break backward compatibilityGravatar Matthieu Sozeau2014-09-24
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Add a tactic [revgoals] to reverse the list of focused goals.Gravatar Arnaud Spiwack2014-09-08
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Remove a redundant typing phase in the [refine] tactic.Gravatar Arnaud Spiwack2014-09-05
* Ltac's [uconstr] values now use the identifier context to give names to binders.Gravatar Arnaud Spiwack2014-09-05
* Moving the decompose tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-09-01
* Removing spurious tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-27
* Add an is_cofix tacticGravatar Jason Gross2014-08-25
* Removing a use of Goal.refine.Gravatar Pierre-Marie Pédrot2014-08-19
* Slight simplification of naming of tactics in equality.ml (hopefully).Gravatar Hugo Herbelin2014-08-18
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
* Better structure for Ltac pretyping environments.Gravatar Pierre-Marie Pédrot2014-08-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 07:56:54 +0000