| Age | Commit message (Expand) | Author |
|---|
| 2002-05-29 | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin |
| 2002-03-04 | Nouveau Rewrite-in plus economique | barras |
| 2002-02-15 | petits changements cosmetiques sur les tactiques | barras |
| 2002-02-11 | substitution et pattern modulo let | barras |
| 2001-12-13 | compat ocaml 3.03 | filliatr |
| 2001-11-05 | GROS COMMIT: | barras |
| 2001-10-11 | Suppression option immediate_discharge; nettoyage de Declare et conséquences | herbelin |
| 2001-10-09 | Suppression des arguments sur les constantes, inductifs et constructeurs | barras |
| 2001-08-28 | Change la constante d'entree de Immediate | mohring |
| 2001-05-31 | Amelioration - subjective - de l'affichage des Hint | herbelin |
| 2001-03-28 | amelioration de la structure des univers | barras |
| 2001-03-15 | entetes | filliatr |
| 2001-03-01 | Déplacement de qualid dans Nametab, hors du noyau | herbelin |
| 2001-02-16 | ident au lieu de string pour le nom de base de qualid | herbelin |
| 2001-02-16 | Prise en compte noms longs dans SuperAuto | herbelin |
| 2001-02-14 | Mise en place d'un système optionnel de discharge immédiat; prise en compte... | herbelin |
| 2001-01-24 | Prise en compte des noms longs dans les Hints et les Coercions, et réorganis... | herbelin |
| 2000-12-26 | Suppression de la beta-iota avant appel de head_pattern_bound, ce sera ce der... | herbelin |
| 2000-12-25 | Normalisation betaiota du pattern avant enregistrement comme hint (certains d... | herbelin |
| 2000-12-12 | Hint Unfold Local + commentaires | mohring |
| 2000-11-24 | certains effets disparaissent a la sortie des sections, d'autres non (selon S... | filliatr |
| 2000-11-23 | print_id, print_sp -> pr_id, pr_sp | herbelin |
| 2000-11-15 | methode export | filliatr |
| 2000-11-10 | Bugs lies a la confusion load/open et a un open abusivement recursif dans lib... | herbelin |
| 2000-11-02 | suppression des (* open Generic *) | filliatr |
| 2000-10-18 | Simplifications autour de typed_type (renommé types par analogie avec sorts)... | herbelin |
| 2000-10-18 | Renommage canonique : | herbelin |
| 2000-10-13 | Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve... | herbelin |
| 2000-10-11 | Prise en compte de l'env local dans make_apply_entry | herbelin |
| 2000-10-06 | Mise en page de Print Hint | herbelin |
| 2000-09-14 | Abstraction de constr | herbelin |
| 2000-09-10 | Correction pour make doc | herbelin |
| 2000-09-10 | Ajout d'un LetIn primitif. | herbelin |
| 2000-07-24 | Passage à des contextes de vars et de rels pouvant contenir des déclarations | herbelin |
| 2000-07-21 | Modifs d'interpretation de patterns | delahaye |
| 2000-06-28 | Modifs de presentation. | delahaye |
| 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 |
| 2000-03-28 | Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf... | herbelin |
| 2000-01-26 | Abstraction de l'implémentation des signatures de Sign en vue intégration d... | herbelin |
| 2000-01-07 | Renommage command en constr | herbelin |
| 1999-12-15 | Nouveaux types 'constructor' et 'inductive' dans Term; | herbelin |
| 1999-12-14 | rattrapage exceptions autres que UserError | filliatr |
| 1999-12-13 | - états fabriqués avec -silent | filliatr |
| 1999-12-13 | - méthode load sur les Hints | filliatr |
| 1999-12-07 | debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkes | filliatr |
| 1999-12-01 | - Typing -> Safe_typing | filliatr |
| 1999-11-24 | Auto,Dhyp,Elim / Reduction de Evar / declarations eliminations | filliatr |
