aboutsummaryrefslogtreecommitdiff
path: root/tactics/eauto.ml4
AgeCommit message (Expand)Author
2010-03-05Fix [autounfold] to accept general [in] clauses.msozeau
2009-11-06Misc fixes.msozeau
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-07-14Simplify eauto and fix it for compatibility, allowing full delta duringmsozeau
2009-07-09Use the proper unification flags in e_exact. This makes exact fail a bitmsozeau
2009-04-08Some dead code removal + cleanupsletouzey
2008-12-28- Another bug in get_sort_family_of (sort-polymorphism of constants andherbelin
2008-12-26- Optimized "auto decomp" which had a (presumably) exponential inherbelin
2008-12-16Finish fix for the treatment of [inverse] in [setoid_rewrite], making amsozeau
2008-12-14Fix looping class resolution bug discovered by B. Aydemir and use themsozeau
2008-09-07Add the ability to declare [Hint Extern]'s with no pattern.msozeau
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-06-27Enhanced discrimination nets implementation, which can now work withmsozeau
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
2008-05-01Move exception-handling code for catching tactics failure msozeau
2008-04-29Fix eauto still using delta when it shouldn't (should make CoRN compilemsozeau
2008-04-28Backtrack on using metas eagerly in auto, only done in "new auto" formsozeau
2008-04-27- Fix bug in unification not taking into account the right metamsozeau
2008-04-24- Add pretty-printers for Idpred, Cpred and transparent_state, used formsozeau
2008-04-21- Parameterize unification by two sets of transparent_state, one for openmsozeau
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-04Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quandherbelin
2008-03-08correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)jforest
2008-02-14Backtrack changes on eauto, move specialized version of eauto inmsozeau
2008-02-13Debugging of the class_setoid tactic and eauto. Prepare for move frommsozeau
2008-02-09Fix the clrewrite tactic, change Relations.v to work on relations in Propmsozeau
2008-02-08Change implementation of resolution for typeclasses to use a customizedmsozeau
2008-02-06Work-in-progress to make eauto accept a list of goals as input andmsozeau
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-07-11Slight cleanup of refl_omega.ml : in particular it uses now listletouzey
2007-05-22Nouvelle stratégie d'unification des types des with-bindings dansherbelin
2007-04-28Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.herbelin
2007-04-16Suite unification apply et eapply (l'un et l'autre profite maintenantherbelin
2007-04-15Essai de partage de code entre apply et eapplyherbelin
2006-10-25Correction d'une tentative incorrecte (révision 9266) de clarificationherbelin
2006-05-30Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...herbelin
2006-04-27Standardisation nom option_app en option_mapherbelin
2006-02-05Debugging en syntaxe v8herbelin
2006-01-28Ajout option 'using lemmas' à auto/trivial/eautoherbelin
2006-01-24Suppression de la dépendance en Map.fold de ocaml dont la sémantique aherbelin
2006-01-19Export eassumptionherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-12-21Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...herbelin
2005-12-02Changement des named_contextgregoire
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par o...herbelin
2004-12-07* added subst_evaluable_referencesacerdot
2004-09-08unification encore...barras
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
2004-09-03premiere reorganisation de l\'unificationbarras