| Age | Commit message (Expand) | Author |
|---|
| 2009-12-24 | Opened the possibility to type Ltac patterns but it is not fully functional yet | herbelin |
| 2009-10-28 | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau |
| 2009-10-21 | This big commit addresses two problems: | soubiran |
| 2009-09-22 | Better use of transparency information for local hypotheses: | msozeau |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-05-09 | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin |
| 2009-03-31 | Fix auto so that Extern tactics associated to no patterns can apply to | msozeau |
| 2008-12-26 | - Optimized "auto decomp" which had a (presumably) exponential in | herbelin |
| 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 |
