aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.ml
Commit message (Expand)AuthorAge
* 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
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* Enhancements to coqdoc, better globalization of sections and modules.Gravatar msozeau2008-06-06
* - Fix bug #1858, Hint Unfold calling the wrong locate function.Gravatar msozeau2008-05-23
* Correct a bug in "new auto" and also unify_eqn which did not do localGravatar msozeau2008-04-30
* Fix eauto still using delta when it shouldn't (should make CoRN compileGravatar msozeau2008-04-29
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
* - Fix bug in unification not taking into account the right metaGravatar msozeau2008-04-27
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 03:49:43 +0000