aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.ml
Commit message (Expand)AuthorAge
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* ident au lieu de string pour le nom de base de qualidGravatar herbelin2001-02-16
* Prise en compte noms longs dans SuperAutoGravatar herbelin2001-02-16
* Mise en place d'un système optionnel de discharge immédiat; prise en compte...Gravatar herbelin2001-02-14
* Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...Gravatar herbelin2001-01-24
* Suppression de la beta-iota avant appel de head_pattern_bound, ce sera ce der...Gravatar herbelin2000-12-26
* Normalisation betaiota du pattern avant enregistrement comme hint (certains d...Gravatar herbelin2000-12-25
* Hint Unfold Local + commentairesGravatar mohring2000-12-12
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
* methode exportGravatar filliatr2000-11-15
* Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...Gravatar herbelin2000-11-10
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Simplifications autour de typed_type (renommé types par analogie avec sorts)...Gravatar herbelin2000-10-18
* Renommage canonique :Gravatar herbelin2000-10-18
* Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...Gravatar herbelin2000-10-13
* Prise en compte de l'env local dans make_apply_entryGravatar herbelin2000-10-11
* Mise en page de Print HintGravatar herbelin2000-10-06
* Abstraction de constrGravatar herbelin2000-09-14
* Correction pour make docGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
* Modifs de presentation.Gravatar delahaye2000-06-28
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
* Introduction d'un type constr_pattern pour les différents filtragesGravatar herbelin2000-04-26
* Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf...Gravatar herbelin2000-03-28
* Abstraction de l'implémentation des signatures de Sign en vue intégration d...Gravatar herbelin2000-01-26
* Renommage command en constrGravatar herbelin2000-01-07
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* rattrapage exceptions autres que UserErrorGravatar filliatr1999-12-14
* - états fabriqués avec -silentGravatar filliatr1999-12-13
* - méthode load sur les HintsGravatar filliatr1999-12-13
* debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesGravatar filliatr1999-12-07
* - Typing -> Safe_typingGravatar filliatr1999-12-01
* Auto,Dhyp,Elim / Reduction de Evar / declarations eliminationsGravatar filliatr1999-11-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 03:45:01 +0000