| Age | Commit message (Expand) | Author |
|---|
| 2008-09-07 | Add the ability to declare [Hint Extern]'s with no pattern. | msozeau |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2008-06-27 | Enhanced discrimination nets implementation, which can now work with | msozeau |
| 2008-06-10 | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin |
| 2008-05-01 | Move exception-handling code for catching tactics failure | msozeau |
| 2008-04-29 | Fix eauto still using delta when it shouldn't (should make CoRN compile | msozeau |
| 2008-04-28 | Backtrack on using metas eagerly in auto, only done in "new auto" for | msozeau |
| 2008-04-27 | - Fix bug in unification not taking into account the right meta | msozeau |
| 2008-04-24 | - Add pretty-printers for Idpred, Cpred and transparent_state, used for | msozeau |
| 2008-04-21 | - Parameterize unification by two sets of transparent_state, one for open | msozeau |
| 2008-04-13 | Bugs, nettoyage, et améliorations diverses | herbelin |
| 2008-04-04 | Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quand | herbelin |
| 2008-03-08 | correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases) | jforest |
| 2008-02-14 | Backtrack changes on eauto, move specialized version of eauto in | msozeau |
| 2008-02-13 | Debugging of the class_setoid tactic and eauto. Prepare for move from | msozeau |
| 2008-02-09 | Fix the clrewrite tactic, change Relations.v to work on relations in Prop | msozeau |
| 2008-02-08 | Change implementation of resolution for typeclasses to use a customized | msozeau |
| 2008-02-06 | Work-in-progress to make eauto accept a list of goals as input and | msozeau |
| 2007-12-05 | Factorisation des opérations sur le type option de Util dans un module | aspiwack |
| 2007-07-11 | Slight cleanup of refl_omega.ml : in particular it uses now list | letouzey |
| 2007-05-22 | Nouvelle stratégie d'unification des types des with-bindings dans | herbelin |
| 2007-04-28 | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin |
| 2007-04-16 | Suite unification apply et eapply (l'un et l'autre profite maintenant | herbelin |
| 2007-04-15 | Essai de partage de code entre apply et eapply | herbelin |
| 2006-10-25 | Correction d'une tentative incorrecte (révision 9266) de clarification | herbelin |
| 2006-05-30 | Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme... | herbelin |
| 2006-04-27 | Standardisation nom option_app en option_map | herbelin |
| 2006-02-05 | Debugging en syntaxe v8 | herbelin |
| 2006-01-28 | Ajout option 'using lemmas' à auto/trivial/eauto | herbelin |
| 2006-01-24 | Suppression de la dépendance en Map.fold de ocaml dont la sémantique a | herbelin |
| 2006-01-19 | Export eassumption | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis... | herbelin |
| 2005-12-21 | Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact... | herbelin |
| 2005-12-02 | Changement des named_context | gregoire |
| 2005-11-08 | Nettoyage suite à la détection par défaut des variables inutilisées par o... | herbelin |
| 2004-12-07 | * added subst_evaluable_reference | sacerdot |
| 2004-09-08 | unification encore... | barras |
| 2004-09-07 | deuxieme vague de modifs: evar_defs fonctionnel | barras |
| 2004-09-03 | premiere reorganisation de l\'unification | barras |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2003-12-01 | Nouvelle tactique EExists | clrenard |
| 2003-11-17 | New tactics : econstructor, eleft, eright, esplit | clrenard |
| 2003-11-08 | Nettoyage | herbelin |
| 2003-08-11 | Nouvelle mouture du traducteur v7->v8 | herbelin |
| 2003-04-07 | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin |
| 2003-03-12 | *** empty log message *** | barras |
| 2003-01-19 | Restructuration interpréteur de tactique: plus d'évaluation partielle à la... | herbelin |
| 2002-12-09 | Option pour rendre les vérifications du refiner optionnelle | herbelin |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-06-05 | Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar... | herbelin |
