aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Expand)AuthorAge
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
* Added "etransitivity".Gravatar herbelin2009-08-03
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* Reimplementation of leibniz rewrite to control the instantiation of theGravatar msozeau2009-06-16
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
* Minor unification changes:Gravatar msozeau2009-05-18
* - Allowing multiple calls to tactic fix with automatic generation ofGravatar herbelin2009-05-17
* Backporting 12080 (fixing bug #2091 on bad rollback in the "where"Gravatar herbelin2009-04-24
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
* Fix auto so that Extern tactics associated to no patterns can apply toGravatar msozeau2009-03-31
* Compromise wrt introduction-names compatibility issue after additionGravatar herbelin2009-03-22
* Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)Gravatar herbelin2009-03-17
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* Add support for dependent "destruct" over terms in dependent types.Gravatar herbelin2009-02-23
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* Fix [apply_in] which short-circuited resolution of evars in a customGravatar msozeau2009-02-16
* pushed evar reduction in kernelGravatar barras2009-02-06
* Report r11631 from 8.2 and handle non-dependent goals better inGravatar msozeau2009-02-04
* Fixed bugs #2001 (search_guard was overwriting the guard index givenGravatar herbelin2009-01-04
* Fixed two problems:Gravatar herbelin2009-01-03
* - Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",Gravatar herbelin2009-01-02
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* - Extracted from the tactic "now" an experimental tactic "easy" for smallGravatar herbelin2008-12-26
* - Fixed cutrewrite bug #2021 introduced in commit 11662 (as a sideGravatar herbelin2008-12-18
* Finish fix for the treatment of [inverse] in [setoid_rewrite], making aGravatar msozeau2008-12-16
* Fixed in bug in previous 11662 (incorrect with_evars flag in descend_conjunct...Gravatar herbelin2008-12-12
* About "apply in":Gravatar herbelin2008-12-09
* closed bug 1898: fold x in x; added a reordering primitive tacticGravatar barras2008-11-26
* - Fixed minor bug #1994 in the tactic chapter of the manual [doc]Gravatar herbelin2008-11-22
* Port [rewrite] tactics to open terms. Currently no check that evarsGravatar msozeau2008-11-05
* Adaptation du vieil appel à "apply" sur lemme de symétrie au cas oùGravatar herbelin2008-10-29
* - Fixed many "Theorem with" bugs.Gravatar herbelin2008-10-27
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
* Fix bug #1977 by allowing the [apply] variants to take an [open_constr]Gravatar msozeau2008-10-23
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* Various little improvements:Gravatar msozeau2008-09-25
* Add a type argument to letin_tac instead of using casts and recomputingGravatar msozeau2008-09-12
* Fixes in dependent induction tactic, putting things in better order forGravatar msozeau2008-09-11
* Fix bug #1935, reworking the reflexivity, symmetry... tactics to useGravatar msozeau2008-09-03
* Fixes in dependent induction tactic to keep names, allow givingGravatar msozeau2008-08-21
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Fixes in generalize_eqs/dependent induction to allow the user to specifyGravatar msozeau2008-07-28
* New tactics [conv] to test convertibility (actually, unification) of twoGravatar msozeau2008-07-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 15:05:46 +0000