aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.ml
Commit message (Expand)AuthorAge
* application patch Cuit Alvarado : tclTHENSi et intros_until_n exportésGravatar filliatr2001-02-01
* Prise en compte des let-in dans les fonctions de réduction pour les tactiquesGravatar herbelin2000-11-27
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Renommage canonique :Gravatar herbelin2000-10-18
* Renommage AppL en AppGravatar herbelin2000-10-01
* 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
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
* Modifs d'interpretation de patternsGravatar delahaye2000-07-21
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
* 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
* Encapsulage de PatternMatchingFailure par un 'error' pour que l'echec de conc...Gravatar herbelin2000-05-03
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* Suite intégration de constr_patternGravatar herbelin2000-04-30
* Déplacement du type reference dans TermGravatar herbelin2000-04-28
* Changement de représentation du contexte des réf dans rawconstr et patternGravatar herbelin2000-04-28
* Introduction d'un type constr_pattern pour les différents filtragesGravatar herbelin2000-04-26
* 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
* debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesGravatar filliatr1999-12-07
* premier debugageGravatar filliatr1999-12-05
* - environment -> safe_environmentGravatar filliatr1999-12-01
* modules Indrec, Tacentries, HiddentacGravatar filliatr1999-11-23
* module WcclausenvGravatar filliatr1999-11-22
* module Tactics (debut)Gravatar filliatr1999-11-22
* module Pattern, Wcclausenv (interface) et TacticalsGravatar filliatr1999-11-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 22:48:49 +0000