aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.ml
AgeCommit message (Expand)Author
2009-04-24Backporting 12080 (fixing bug #2091 on bad rollback in the "where"herbelin
2009-04-10Fix premature optimisation in dependent induction: even variable args needmsozeau
2009-03-31Fix auto so that Extern tactics associated to no patterns can apply tomsozeau
2009-03-22Compromise wrt introduction-names compatibility issue after additionherbelin
2009-03-17Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)herbelin
2009-03-16Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"herbelin
2009-03-14Cleaning/uniformizing the interface of tacticals.mliherbelin
2009-02-23Add support for dependent "destruct" over terms in dependent types.herbelin
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2009-02-16Fix [apply_in] which short-circuited resolution of evars in a custommsozeau
2009-02-06pushed evar reduction in kernelbarras
2009-02-04Report r11631 from 8.2 and handle non-dependent goals better inmsozeau
2009-01-04Fixed bugs #2001 (search_guard was overwriting the guard index givenherbelin
2009-01-03Fixed two problems:herbelin
2009-01-02- Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",herbelin
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
2008-12-29- Added support for subterm matching in SearchAbout.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-12-18- Fixed cutrewrite bug #2021 introduced in commit 11662 (as a sideherbelin
2008-12-16Finish fix for the treatment of [inverse] in [setoid_rewrite], making amsozeau
2008-12-12Fixed in bug in previous 11662 (incorrect with_evars flag in descend_conjunct...herbelin
2008-12-09About "apply in":herbelin
2008-11-26closed bug 1898: fold x in x; added a reordering primitive tacticbarras
2008-11-22- Fixed minor bug #1994 in the tactic chapter of the manual [doc]herbelin
2008-11-05Port [rewrite] tactics to open terms. Currently no check that evarsmsozeau
2008-10-29Adaptation du vieil appel à "apply" sur lemme de symétrie au cas oùherbelin
2008-10-27- Fixed many "Theorem with" bugs.herbelin
2008-10-26Fixes and refinements regarding occurrence selection:herbelin
2008-10-26Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiherbelin
2008-10-23Fix bug #1977 by allowing the [apply] variants to take an [open_constr]msozeau
2008-10-18Optimisation de clenv.ml pour que meta_instance ne soit pas appeléherbelin
2008-09-25Various little improvements:msozeau
2008-09-12Add a type argument to letin_tac instead of using casts and recomputingmsozeau
2008-09-11Fixes in dependent induction tactic, putting things in better order formsozeau
2008-09-03Fix bug #1935, reworking the reflexivity, symmetry... tactics to usemsozeau
2008-08-21Fixes in dependent induction tactic to keep names, allow givingmsozeau
2008-08-04Évolutions diverses et variées.herbelin
2008-07-28Fixes in generalize_eqs/dependent induction to allow the user to specifymsozeau
2008-07-22New tactics [conv] to test convertibility (actually, unification) of twomsozeau
2008-07-18Modification rapide du message d'erreur lorsqu'un _ ne peut êtreherbelin
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2008-06-18Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkherbelin
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
2008-06-10Backtrack sur l'"optimisation" de admit (révision 11084). Comme leherbelin
2008-06-10- Correction bug 1841 (identificateurs incorrects avec Subclass)herbelin
2008-06-08- Patch sur "intros until 0"herbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-05-30Improve the dependent induction tactic to automatically find themsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 04:54:29 +0000