| Age | Commit message (Expand) | Author |
|---|
| 2008-09-07 | Add the ability to declare [Hint Extern]'s with no pattern. | msozeau |
| 2008-09-07 | Fixes in typeclasses resolution. Avoid reducing instances types before | msozeau |
| 2008-09-04 | Improve typeclasses eauto using the dnet for local assumptions too, and select | msozeau |
| 2008-08-27 | Little cleanup in auto. | msozeau |
| 2008-08-22 | - New auto hints for transparency/opacity control, not bound to | msozeau |
| 2008-06-27 | Enhanced discrimination nets implementation, which can now work with | 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-21 | - Parameterize unification by two sets of transparent_state, one for open | msozeau |
| 2008-04-04 | Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quand | herbelin |
| 2008-03-06 | Syntax changes in typeclasses, remove "?" for usual implicit arguments | msozeau |
| 2007-09-30 | Ajout infos de débogage de "universe inconsistency" quand option Set | herbelin |
| 2006-01-28 | Ajout option 'using lemmas' à auto/trivial/eauto | herbelin |
| 2006-01-28 | Suppression code pour hints nommés à la V7 (voire à la V6...) | herbelin |
| 2006-01-24 | Suppression de la dépendance en Map.fold de ocaml dont la sémantique a | herbelin |
| 2005-01-21 | Compatibilité ocamlweb pour cible doc | herbelin |
| 2004-12-07 | * added subst_evaluable_reference | sacerdot |
| 2004-12-07 | The type Pattern.constr_label was isomorphic to Libnames.global_reference. | sacerdot |
| 2004-11-16 | Names.substitution (and related functions) and Term.subst_mps moved to | sacerdot |
| 2004-09-10 | simplification de clenv | barras |
| 2004-09-08 | unification encore... | barras |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2003-06-14 | Ajout option Local à Hint, Hints et HintDestruct | herbelin |
| 2003-05-19 | Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern | herbelin |
| 2003-04-07 | Globalisation des noms de tactiques dans les définitions de tactiques | herbelin |
| 2002-11-14 | Réforme de l'interprétation des termes : | herbelin |
| 2002-08-02 | Modules dans COQ\!\!\!\! | coq |
| 2002-05-29 | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin |
| 2001-11-06 | Suppression des local_constraints, des ctxtty et du focus. | clrenard |
| 2001-11-05 | GROS COMMIT: | barras |
| 2001-03-15 | entetes | filliatr |
| 2001-02-26 | Eauto version en largeur | mohring |
| 2001-02-16 | Prise en compte noms longs dans SuperAuto | herbelin |
| 2001-01-24 | Prise en compte des noms longs dans les Hints et les Coercions, et réorganis... | herbelin |
| 2000-12-12 | syntaxe AST Inversion + commentaires ocamlweb autour de $ | filliatr |
| 2000-10-18 | Renommage canonique : | herbelin |
| 2000-10-11 | Prise en compte de l'env local dans make_apply_entry | herbelin |
| 2000-07-24 | Passage à des contextes de vars et de rels pouvant contenir des déclarations | herbelin |
| 2000-05-03 | Ajout du langage de tactiques | delahaye |
| 2000-04-28 | Déplacement du type reference dans Term | herbelin |
| 2000-04-26 | Introduction d'un type constr_pattern pour les différents filtrages | herbelin |
| 1999-12-07 | debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkes | filliatr |
| 1999-12-05 | premier debugage | filliatr |
| 1999-11-24 | Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations | filliatr |
