aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/eauto.ml4
Commit message (Expand)AuthorAge
* Misc fixes.Gravatar msozeau2009-11-06
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Simplify eauto and fix it for compatibility, allowing full delta duringGravatar msozeau2009-07-14
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-07-09
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* - 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
* Finish fix for the treatment of [inverse] in [setoid_rewrite], making aGravatar msozeau2008-12-16
* Fix looping class resolution bug discovered by B. Aydemir and use theGravatar msozeau2008-12-14
* Add the ability to declare [Hint Extern]'s with no pattern.Gravatar msozeau2008-09-07
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* Move exception-handling code for catching tactics failure Gravatar msozeau2008-05-01
* 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
* - Fix bug in unification not taking into account the right metaGravatar msozeau2008-04-27
* - Add pretty-printers for Idpred, Cpred and transparent_state, used forGravatar msozeau2008-04-24
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quandGravatar herbelin2008-04-04
* correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)Gravatar jforest2008-03-08
* Backtrack changes on eauto, move specialized version of eauto inGravatar msozeau2008-02-14
* Debugging of the class_setoid tactic and eauto. Prepare for move fromGravatar msozeau2008-02-13
* Fix the clrewrite tactic, change Relations.v to work on relations in PropGravatar msozeau2008-02-09
* Change implementation of resolution for typeclasses to use a customizedGravatar msozeau2008-02-08
* Work-in-progress to make eauto accept a list of goals as input andGravatar msozeau2008-02-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Slight cleanup of refl_omega.ml : in particular it uses now listGravatar letouzey2007-07-11
* Nouvelle stratégie d'unification des types des with-bindings dansGravatar herbelin2007-05-22
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* Suite unification apply et eapply (l'un et l'autre profite maintenantGravatar herbelin2007-04-16
* Essai de partage de code entre apply et eapplyGravatar herbelin2007-04-15
* Correction d'une tentative incorrecte (révision 9266) de clarificationGravatar herbelin2006-10-25
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Debugging en syntaxe v8Gravatar herbelin2006-02-05
* Ajout option 'using lemmas' à auto/trivial/eautoGravatar herbelin2006-01-28
* Suppression de la dépendance en Map.fold de ocaml dont la sémantique aGravatar herbelin2006-01-24
* Export eassumptionGravatar herbelin2006-01-19
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...Gravatar herbelin2005-12-21
* Changement des named_contextGravatar gregoire2005-12-02
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* * added subst_evaluable_referenceGravatar sacerdot2004-12-07
* unification encore...Gravatar barras2004-09-08
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16