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