aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.ml
Commit message (Expand)AuthorAge
* Solved a few problems of auto by bypassing the call to apply.Gravatar herbelin2010-04-17
* Use nice "unfold" instead of ugly "change" to display calls to unfold hintsGravatar herbelin2010-04-17
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
* Added module sharing support for typeclasses and hints (pri_auto_tactic).Gravatar soubiran2010-01-12
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* Backtrack on making exact hints for lemmas starting with productsGravatar msozeau2009-12-19
* Fix make_exact_entry to allow applying [forall x, P x] hints directly,Gravatar msozeau2009-12-01
* Lazier behaviour of [auto] when introducing hypothesis: query the hint db's o...Gravatar puech2009-11-21
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Removal of trailing spaces.Gravatar serpyc2009-10-04
* Remove legacy export_* functionsGravatar glondu2009-09-29
* Better use of transparency information for local hypotheses: Gravatar msozeau2009-09-22
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* - 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
* Simplify addition of hints to a hint_db. Rebuild the dnet associatedGravatar msozeau2009-07-08
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Minor unification changes:Gravatar msozeau2009-05-18
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Fix auto so that Extern tactics associated to no patterns can apply toGravatar msozeau2009-03-31
* 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
* 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
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-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
* Add the ability to declare [Hint Extern]'s with no pattern.Gravatar msozeau2008-09-07
* Fixes in typeclasses resolution. Avoid reducing instances types beforeGravatar msozeau2008-09-07
* Improve typeclasses eauto using the dnet for local assumptions too, and selectGravatar msozeau2008-09-04
* Little cleanup in auto.Gravatar msozeau2008-08-27
* - New auto hints for transparency/opacity control, not bound to Gravatar msozeau2008-08-22
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Suite commit 11236Gravatar notin2008-07-24
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...Gravatar notin2008-07-18
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Fix implicit arguments in sections bug and check for resolution of evars whenGravatar msozeau2008-07-07
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 22:42:33 +0000