aboutsummaryrefslogtreecommitdiff
path: root/theories/Init/Tactics.v
AgeCommit message (Expand)Author
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-10-15Report a useful error for dependent destructionTej Chajed
2020-08-25Modify Classes/RelationClasses.v to compile with -mangle-namesJasper Hugunin
2020-08-25Modify Init/Tactics.v to compile with -mangle-namesJasper Hugunin
2020-04-21Moving the main Require Export Ltac in Prelude.v.Hugo Herbelin
2020-03-19Merge PR #11822: Grants #11692: clear dependent knows about let-inPierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-14Fixes #11692 (clear dependent knows about let-in).Hugo Herbelin
2019-10-29Use a less kludgy way of solving #9114Jason Gross
2019-10-29Fix #9114, assert_succeeds (exact I) solves goalJason Gross
2019-10-29`assert_succeeds`&`assert_fails`: multisuccess fixJason Gross
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-25Modifying theories to preferably use the "[= ]" syntax, and,Hugo Herbelin
2019-03-26Declare initial hint databases in preludeMaxime Dénès
2019-01-23Pass some files to strict focusing mode.Gaëtan Gilbert
2018-03-09Merge PR #6820: Tacticals assert_fails and assert_succeedsMaxime Dénès
2018-02-28Uniform spacing layout in Tactics.v.Hugo Herbelin
2018-02-28Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).Hugo Herbelin
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-14Add named timers to LtacProfJason Gross
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-05-28Add equality lemmas for sig2 and sigT2Jason Gross
2017-05-28Add an [inversion_sigma] tacticJason Gross
2017-05-03Report a useful error for dependent inductionTej Chajed
2016-07-18Remove the swap tactic from the prelude.Maxime Dénès
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-01-20Update copyright headers.Maxime Dénès
2015-02-25Reorder the steps of the easy tactic. (Fix for bug #2630)Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-08-25"allows to", like "allowing to", is improperJason Gross
2012-08-08Updating headers.herbelin
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
2011-05-05Modularization of BinNat + fixes of stdlibletouzey
2011-04-28Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixedherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-16Bool: shorter and more systematic proofs + an iff lemma about eqbletouzey
2010-06-18clear/revert dependent: restrict to hyp(h) instead of ident(h)letouzey
2010-06-17New tactic "clear dependent", for the moment in ltac in Init/Tacticsletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-08Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'letouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-24New tactic to rewrite decidability lemmas when one knows which sideherbelin
2009-06-29Miscellaneous practical commits: herbelin
2009-01-02- Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",herbelin
2008-12-28- Another bug in get_sort_family_of (sort-polymorphism of constants andherbelin
2008-12-26- Extracted from the tactic "now" an experimental tactic "easy" for smallherbelin
2008-08-05Correction de bugs:herbelin
2008-08-04Évolutions diverses et variées.herbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:15:20 +0000