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