aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tacinterp.ml
Commit message (Expand)AuthorAge
* Suite de la suppression : enamed_declaration est remplace par evar_map.Gravatar clrenard2001-11-06
* GROS COMMIT:Gravatar barras2001-11-05
* Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRGravatar delahaye2001-10-23
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
* Ajout de dynamiques pour les quotations constr et tacticGravatar delahaye2001-10-02
* Ajout du printer de tactiques + modif du Dynamic ocamlGravatar delahaye2001-09-30
* Changement du message d'erreur pour l'interpreteur de tactiquesGravatar delahaye2001-09-24
* Correction due au changement de semantique de MatchGravatar delahaye2001-09-21
* TransparentGravatar barras2001-09-20
* ParsingGravatar herbelin2001-08-10
* Changements dans le traitement des qualid'sGravatar delahaye2001-07-19
* Evar et Zeta ne sont plus implicites dans Delta (mais le restent dans Compute...Gravatar herbelin2001-07-02
* Nettoyage/restructuration des ensembles d'indicateurs de réductionsGravatar herbelin2001-07-02
* Backtracking pour le MatchGravatar delahaye2001-06-29
* Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...Gravatar herbelin2001-06-25
* Extension des parametres de Clear + InstGravatar delahaye2001-06-19
* Interpretation MetaId + Progress + InstGravatar delahaye2001-06-18
* quelques bug reports mineursGravatar barras2001-05-07
* Metas dans les Unfold'sGravatar delahaye2001-04-19
* Ajout de _ dans les patterns d'introGravatar mohring2001-04-12
* utilisation de Options.if_verboseGravatar filliatr2001-04-03
* amelioration de la structure des universGravatar barras2001-03-28
* entetesGravatar filliatr2001-03-15
* 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
* Reparation du pretty-print pour les tactiquesGravatar delahaye2001-02-07
* Correction pour les Unfold/Fold dans CbvGravatar delahaye2001-02-06
* Mise en place de la possibilite d'unfolder des variables locales et des const...Gravatar filliatr2001-01-31
* Meta Definition + Tactic DefinitionGravatar delahaye2001-01-09
* Arite cachee de Match Context + Meta DefinitionGravatar delahaye2001-01-05
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
* Correction pour les variables abstraites dans les Tactic DefinitionsGravatar delahaye2000-12-19
* Portage d'AutoRewriteGravatar delahaye2000-12-02
* Elimination du 'Gravatar delahaye2000-11-28
* Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au evaluable...Gravatar herbelin2000-11-27
* certains effets disparaissent a la sortie des sections, d'autres non (selon S...Gravatar filliatr2000-11-24
* Correction d'un bug lorsque des Variables sont clearees dans le but courantGravatar delahaye2000-11-23
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 's...Gravatar herbelin2000-11-22
* Tout est deja traite dans TacinterpGravatar delahaye2000-11-21
* Traitement du pretty-print des RedexpGravatar delahaye2000-11-21
* Prise en compte noms longsGravatar herbelin2000-11-20
* methode exportGravatar filliatr2000-11-15
* Bugs lies a la confusion load/open et a un open abusivement recursif dans lib...Gravatar herbelin2000-11-10
* Modification de la table des tactic Definitions pour eviter l'ecritureGravatar mohring2000-11-07
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
* Tactiques utilisateur + debuggerGravatar delahaye2000-10-30
* Clarification message d'erreurGravatar herbelin2000-10-28
* Renommage canonique :Gravatar herbelin2000-10-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 18:12:36 +0000