aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Expand)AuthorAge
* Remplacement des hacks pour les noms longs par un appel à Declare.global_qua...Gravatar herbelin2000-11-20
* Bug et simplification nouvel InductionGravatar herbelin2000-11-09
* Nettoyage Names suiteGravatar herbelin2000-11-07
* Marre de ces noms stupides IAvoid and co; changé en IntroAvoid and co; bah.....Gravatar herbelin2000-11-06
* nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...Gravatar filliatr2000-11-06
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* erreur dans intro_gen corrigéeGravatar filliatr2000-10-27
* Intro choue si le nom d'hypothse existe au lieu de mettre un avertissementGravatar herbelin2000-10-27
* Renommage canonique :Gravatar herbelin2000-10-18
* Suppression du test de convertibilite inutile pour la plupart des exact; 2 ve...Gravatar herbelin2000-10-13
* Bug de conflit de nommage d'hyp d'induction dans l'Induction fonctionnant dan...Gravatar herbelin2000-10-05
* Rebranchement de la tactique LetGravatar herbelin2000-10-03
* Renommage AppL en AppGravatar herbelin2000-10-01
* Plus de whd_castapp_stackGravatar herbelin2000-10-01
* Abstraction de constrGravatar herbelin2000-09-14
* Modification mkAppL; abstraction via kind_of_term; changement dans ReductionGravatar herbelin2000-09-12
* Correction pour make docGravatar herbelin2000-09-10
* Suppression de AbstGravatar herbelin2000-09-10
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
* messages d'erreurGravatar herbelin2000-07-28
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* RienGravatar herbelin2000-06-29
* Déplacement de save_thm and co de PFedit vers CommandGravatar herbelin2000-05-25
* Effets de bords suite à la restructuration des inductives (cf Inductive)Gravatar herbelin2000-05-18
* Retrait du i pour tclTHEN_i et correction bugs DecomposeGravatar herbelin2000-05-16
* Achèvement nettoyage Pfedit; ajout intros_replacingGravatar herbelin2000-05-05
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
* Reparation du bug d'interpretation d'AbstractGravatar delahaye2000-05-03
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
* Nettoyage de l'interface d'Astterm; renommage des {pf_,}constr_of_com* en {pf...Gravatar herbelin2000-03-28
* MAJ ocaml 2.99 (espaces dans la syntaxe des cast)Gravatar herbelin2000-01-26
* Abstraction de l'implémentation des signatures de Sign en vue intégration d...Gravatar herbelin2000-01-26
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
* rattrapage exceptions autres que UserErrorGravatar filliatr1999-12-14
* - global_reference traite des variablesGravatar filliatr1999-12-03
* modifs pour premiere edition de liensGravatar filliatr1999-12-02
* module Tactics (debut)Gravatar filliatr1999-11-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 09:36:56 +0000